Continuations and Martin-Löf's type theory : a thesis presented in partial fulfilment of the requirements of the degree of Doctor of Philosophy in Computer Science at Massey University, Albany, New Zealand

Thumbnail Image
Open Access Location
Journal Title
Journal ISSN
Volume Title
Massey University
The Author
M-LTT is a theory designed to formalize constructive mathematics. By appealing to the Curry-Howard 'propositions as types' analogy, and to the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic we can treat M-LTT as a framework for the specification and derivation of correct functional programs. However, programming in M-LTT has two weaknesses: we are limited in the functions that we can naturally express; the functions that we do write naturally are often inefficient. Programming with continuations allows us partially to address these problems. The continuation-passing programming style is known to offer a number of advantages to the functional programmer. We can also observe a relationship between continuation passing and type lifting in categorial grammar. We present computation rules which allow us to use continuations with inductively-defined types, and with types not presented inductively. We justify the new elimination rules using the usual proof-theoretic semantics. We show that the new rules preserve the consistency of the theory. We show how to use well-orderings to encode continuation-passing operators for inductively defined types.
Functional programming, Type theory, Continuations, Computer science