Ebook: Semantics of Type Theory: Correctness, Completeness and Independence Results
Author: Thomas Streicher (auth.)
- Tags: Computational Science and Engineering, Computational Mathematics and Numerical Analysis, Math Applications in Computer Science, Mathematics of Computing
- Series: Progress in Theoretical Computer Science
- Year: 1991
- Publisher: Birkhäuser Basel
- Edition: 1
- Language: English
- 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.
Content:
Front Matter....Pages i-xii
Introduction....Pages 1-42
Contextual Categories and Categorical Semantics of Dependent Types....Pages 43-111
Models for the Calculus of Constructions and Its Extensions....Pages 112-155
Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions....Pages 156-220
The Term Model of the Calculus of Constructions and Its Metamathematical Applications....Pages 221-264
Related Work, Extensions and Directions of Further Investigations....Pages 265-280
Back Matter....Pages 281-299
Content:
Front Matter....Pages i-xii
Introduction....Pages 1-42
Contextual Categories and Categorical Semantics of Dependent Types....Pages 43-111
Models for the Calculus of Constructions and Its Extensions....Pages 112-155
Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions....Pages 156-220
The Term Model of the Calculus of Constructions and Its Metamathematical Applications....Pages 221-264
Related Work, Extensions and Directions of Further Investigations....Pages 265-280
Back Matter....Pages 281-299
....