Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: A Non-Type-Theoretic Definition of Martin-Lof's Types
Authors: Allen, Stuart
Keywords: computer science
technical report
Issue Date: Apr-1987
Publisher: Cornell University
Abstract: It is possible to make a natural non-type-theoretic reinterpretation of Martin-Lof's type theory. This paper presents an inductive definition of the types explicitly defined in Martin-Lof's paper, Constructive Mathematics and Computer Programming. The definition is set-theoretically valid, and probably will be convincing to intuitionists as well. When this definition is used with methods set out in the author's thesis, the inference rules presented in Martin-Lof's paper can be shown to be valid under the non-type-theoretic interpretation. This interpretation is non-trivial, that is, there are both inhabited types and empty types, and so, validity entails simple consistency. Finally, Michael Beeson has defined some recursive realizability models which we shall compare with the term model presented here, and we shall compare the methods of definition.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
87-832.pdf1.1 MBAdobe PDFView/Open
87-832.ps250.09 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us