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)
PDF
Language: English
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
|
|
Download this file (PDF/1MB) |
![]() |
Postscript
Language: English
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
|
|
Download this file (Postscript/1MB) |
Preview |
Official URL: https://doi.org/10.22024/UniKent/01.02.86128 |
Abstract
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 (https://creativecommons.org/licenses/by-nc-nd/4.0/) 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 (https://www.kent.ac.uk/is/strategy/docs/Kent%20Open%20Access%20policy.pdf). 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 ResearchSupport@kent.ac.uk and we will seriously consider your claim under the terms of our Take-Down Policy (https://www.kent.ac.uk/is/regulations/library/kar-take-down-policy.html). |
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: | https://kar.kent.ac.uk/id/eprint/86128 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):