Skip to main content

Static analysis of Martin-Löf's intuitionistic type theory

Telford, Alastair J. (1995) Static analysis of Martin-Löf's intuitionistic type theory. Doctor of Philosophy (PhD) thesis, University of Kent. (doi:10.22024/UniKent/01.02.86128) (KAR id:86128)

Language: English

Click to download this file (1MB)
[thumbnail of thesis.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Language: English

Click to download this file (1MB) Preview
[thumbnail of]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


Martin-Löf's intuitionistic type theory has been under investigation in recent years as a potential source for future functional programming languages. This is due to its properties which greatly aid the derivation of provably correct programs. These include the Curry-Howard correspondence (whereby logical formulas may be seen as specifications and proofs of logical formulas as programs) and strong normalisation (i.e. evaluation of every proof/program must terminate). Unfortunately, a corollary of these properties is that the programs may contain computationally irrelevant proof objects: proofs which are not to be printed as part of the result of a program.

We show how a series of static analyses may be used to improve the efficiency of type theory as a lazy functional programming language. In particular we show how variants of abstract interpretation may be used to eliminate unnecessary computations in the object code that results from a type theoretic program.

After an informal treatment of the application of abstract interpretation to type theory (where we discuss the features of type theory which make it particularly amenable to such an approach), we give formal proofs of correctness of our abstract interpretation techniques, with regard to the semantics of type theory.

We subsequently describe how we have implemented abstract interpretation techniques within the Ferdinand functional language compiler. Ferdinand was developed as a lazy functional programming system by Andrew Douglas at the University of Kent at Canterbury.

Finally, we show how other static analysis techniques may be applied to type theory. Some of these techniques use the abstract interpretation mechanisms previously discussed.

Item Type: Thesis (Doctor of Philosophy (PhD))
DOI/Identification number: 10.22024/UniKent/01.02.86128
Additional information: This thesis has been digitised by EThOS, the British Library digitisation service, for purposes of preservation and dissemination. It was uploaded to KAR on 09 February 2021 in order to hold its content and record within University of Kent systems. It is available Open Access using a Creative Commons Attribution, Non-commercial, No Derivatives ( licence so that the thesis and its author, can benefit from opportunities for increased readership and citation. This was done in line with University of Kent policies ( If you feel that your rights are compromised by open access to this thesis, or if you would like more information about its availability, please contact us at and we will seriously consider your claim under the terms of our Take-Down Policy (
Uncontrolled keywords: computer programming; Martin-Löf's intuitionistic type theory
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
SWORD Depositor: SWORD Copy
Depositing User: SWORD Copy
Date Deposited: 29 Oct 2019 16:29 UTC
Last Modified: 09 Dec 2022 09:18 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.