Skip to main content


eCommons@Cornell

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

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6706
Title: A Non-Type-Theoretic Semantics For Type-Theoretic Language
Authors: Allen, Stuart
Keywords: computer science
technical report
Issue Date: Sep-1987
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-866
Abstract: Since 1970 several methods have been proposed for using formal systems of constructive logic as programming languages. One prominent approach is based upon systems of computationally significant terms which either bear or are assigned types; these systems are essentially lambda calculi or combinatory logics in which either the terms are explicitly typed or else types are assigned to untyped terms in the manner of Curry. This thesis concerns two such systems, namely, Martin-Lof's intuitionistic type theory of 1979, and a variation of that theory upon which Nuprl is based. Nuprl is a system implemented at Cornell for developing functional programs and constructive proofs. The expressive machinery of these theories can be given a rather natural non-type-theoretic semantics that is not inherently constructive and yet closely follows the semantical explanation of type theory. The principal content of this thesis is a careful development of such a semantic reinterpretation with the intention of making the bulk of type-theoretic practice, of the kind arising from the use of Nuprl and formalizations of Martin-Lof's theory, independent of its original type-theoretic and constructive basis. The reinterpretation opens the type-theoretic methodology of programming to nonconstructivists and others who may not subscribe to the intuitionistic theory of types, preserving the features of type-theoretic language that make it a suitable language for programming. Moreover, the natural structural similarity between the type-theoretic concepts and their reinterpretations yields an analytic tool which may serve type-theorists as well. The body of this thesis has two phases. In the first, the semantic concepts of Martin-Lof's theory, including expressions, types, judgements of functionality, and universes, are reinterpreted. This phase culminates in a non-type-theoretic definition of the types explicitly defined in Martin-Lof's paper of 1979. The remainder of the thesis treats various topics of semantic significance, including the representation of propositions as types, the anticipation of new terms and types, certain "type-free" forms of inference, and a sort of "universe polymorphism." Finally, we shall reinterpret the semantics of Nuprl's judgements of functionality which differs radically from that of Martin-Lof's judgements in the use of assumptions.
URI: http://hdl.handle.net/1813/6706
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
87-866.pdf8.85 MBAdobe PDFView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us