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
Loading...
Date
2000
DOI
Open Access Location
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Massey University
Rights
The Author
Abstract
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.
Description
Keywords
Functional programming, Type theory, Continuations, Computer science