A Non-Type-Theoretic Semantics For Type-Theoretic Language

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