Skip to main content
main-content

Über dieses Buch

Typing plays an important role in software development. Types can be consid­ ered as weak specifications of programs and checking that a program is of a certain type provides a verification that a program satisfies such a weak speci­ fication. By translating a problem specification into a proposition in constructive logic, one can go one step further: the effectiveness and unifonnity of a con­ structive proof allows us to extract a program from a proof of this proposition. Thus by the "proposition-as-types" paradigm one obtains types whose elements are considered as proofs. Each of these proofs contains a program correct w.r.t. the given problem specification. This opens the way for a coherent approach to the derivation of provably correct programs. These features have led to a "typeful" programming style where the classi­ cal typing concepts such as records or (static) arrays are enhanced by polymor­ phic and dependent types in such a way that the types themselves get a complex mathematical structure. Systems such as Coquand and Huet's Calculus of Con­ structions are calculi for computing within extended type systems and provide a basis for a deduction oriented mathematical foundation of programming. On the other hand, the computational power and the expressive (impred­ icativity !) of these systems makes it difficult to define appropriate semantics.

Inhaltsverzeichnis

Frontmatter

Introduction

Abstract
When studying the semantics of constructive logic and constructive mathematics the usual model theoretic semantics for classical logic and mathematics based on naive set theory does not work. The reason is that the basic notion of truth, adequate for classical logic, is not adequate for constructive or intuitionistic logic. When reasoning constructively it is not relevant whether a proposition is true or false but whether it has a proof or not.
Thomas Streicher

Chapter 1. Contextual Categories and Categorical Semantics of Dependent Types

Abstract
By 1978, John Cartmell has introduced the notion of a contextual category in his Ph.D.Thesis on Generalised Algebraic Theories and Contextual Categories [Cartl], part of which has been published as [Cart2]. We give a detailed exposition of his work on contextual categories in order to be able to explain our notion of categorical model for the Calculus of Constructions which is based on Cartmell’s notion of contextual category.
Thomas Streicher

Chapter 2. Models for the Calculus of Constructions and Its Extensions

Abstract
E. Moggi [Mo] (for a recent paper version of Moggi’s original ideas see [LoMo]) has introduced for any partial combinatory algebra D, see e.g. [Be], the category D-Set of D-sets and realizable morphisms between D-sets as a structure where to define a model for the polymorphic λ-calculus by using the D-set of all partial equivalence relations on D as the type of propositions. E. Moggi’s ideas are based on previous work on a topos-theoretic account of Kleene’s notion of realisability following suggestions of Dana Scott and developed to a considerable amount by the group around M. Hyland and A. Pitts in Cambridge, see e.g. [Hy].
Thomas Streicher

Chapter 3. Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions

Abstract
According to Gerard Huet and Thierry Coquand the Calculus of Constructions is a typed λ-calculus where type expressions themselves can contain λ-expressions as subterms. The original presentation in [Col] is characterized by a lot of overloading which has puzzled many readers as there products of types, functional abstraction and universal quantification were represented by one and the same syntactic construct, namely [x:A]B. Another instance of overloading was their systematic mixing of two aspects of propositions, namely propositions as objects of type Prop and propositions as types. This ambiguity we avoid by the type-forming construct Proof, which when applied to an object p of type Prop gives the type Proof(p) of proofs of the proposition p.
Thomas Streicher

Chapter 4. The Term Model of the Calculus of Constructions and Its Metamathematical Applications

Abstract
The aim of this chapter is to construct a doctrine of constructions C I as a term model of the Calculus of Constructions such that the interpretation in this model interprets only provably well-defined contexts, types and objects and identifies only those contexts, types or objects which are provably equal up to renaming of variables bound in the contexts.
Thomas Streicher

Related Work, Extensions and Directions of Further Investigations

Abstract
In the previous chapters we have studied the Calculus of Constructions following a classical pattern. We have introduced a class of structures called doctrines of constructions in Chapter 1 and studied several instances of this notion in Chapter 2 (realizability and retract models). In Chapter 3 we have defined an axiomatization of the calculus and the interpretation of this calculus in arbitrary doctrines of constructions and then have proved a correctness theorem. Finally in Chapter 4 we have shown the existence of a term model. Further we have shown that only provably correct types and objects get an interpretation in the term model and only those equality judgments which can be derived in the calculus are valid under interpretation in the term model.
Thomas Streicher

Backmatter

Weitere Informationen