Semantics of Type Theory

1. Front Matter

   Pages i-xii

   PDF

2. Introduction

   • Thomas Streicher

   Pages 1-42

3. Contextual Categories and Categorical Semantics of Dependent Types

   • Thomas Streicher

   Pages 43-111

4. Models for the Calculus of Constructions and Its Extensions

   • Thomas Streicher

   Pages 112-155

5. Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions

   • Thomas Streicher

   Pages 156-220

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

   • Thomas Streicher

   Pages 221-264

7. Related Work, Extensions and Directions of Further Investigations

   • Thomas Streicher

   Pages 265-280

8. Back Matter

   Pages 281-299

   PDF

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.

• Mathematica
• logic
• programming
• software development
• verification

• Fakultat für Mathematik und Informatik, Universität Passau, Passau, Germany

  Thomas Streicher

Policies and ethics