Static Analysis of Martin-L''of's Intuitionistic Type Theory

Telford, Alastair (1995) Static Analysis of Martin-L''of's Intuitionistic Type Theory. Doctor of Philosophy (Ph.D.) thesis, The Computing Laboratory, University of Kent at Canterbury. (Full text available)

PDF
Download (1MB)
[img]
Preview
Postscript
Download (1MB)
[img]
Preview

Abstract

Martin-Lof'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. abstract

Item Type: Thesis (Doctor of Philosophy (Ph.D.))
Uncontrolled keywords: Type Theory, Functional Programming, Computational Redundancy, Abstract Interpretation
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 19 Aug 2009 19:44
Last Modified: 06 Sep 2011 03:47
Resource URI: http://kar.kent.ac.uk/id/eprint/21246 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year