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

Simple item page
dc.contributor.authorLeslie, Neil
dc.date.accessioned2011-06-24T03:52:38Z
dc.date.available2011-06-24T03:52:38Z
dc.date.issued2000
dc.description.abstractM-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.en_US
dc.identifier.urihttp://hdl.handle.net/10179/2456
dc.language.isoenen_US
dc.publisherMassey Universityen_US
dc.rightsThe Authoren_US
dc.subjectFunctional programmingen_US
dc.subjectType theoryen_US
dc.subjectContinuationsen_US
dc.subjectComputer scienceen_US
dc.titleContinuations 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 Zealanden_US
dc.typeThesisen_US
massey.contributor.authorLeslie, Neil
thesis.degree.disciplineComputer Science
thesis.degree.grantorMassey University
thesis.degree.levelDoctoral
thesis.degree.levelDoctoralen
thesis.degree.nameDoctor of Philosophy (Ph.D.)
Files
Original bundle
Now showing 1 - 2 of 2
Thumbnail Image
Name:
01_front.pdf
Size:
1.16 MB
Format:
Adobe Portable Document Format
Description:
Download
Thumbnail Image
Name:
02_whole.pdf
Size:
3.7 MB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
804 B
Format:
Item-specific license agreed upon to submission
Description:
Download
Collections
Theses and Dissertations