By

MartinLofs 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 CurryHoward correspondence whereby logical formulas may be seen as speci cations and proofs of logical formulas as programs and strong normal isation ie evaluation of every proofprogram 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 eciency 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 particu larly 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 discusse