Semantics of Type Theory Correctness, Completeness and Independence Results
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 propositio...
| Main Author: | |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Boston, MA
Birkhäuser
1991, 1991
|
| Edition: | 1st ed. 1991 |
| Series: | Progress in Theoretical Computer Science
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- 1 Contextual Categories and Categorical Semantics of Dependent Types
- 2 Models for the Calculus of Constructions and Its Extensions
- 3 Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions
- 4 The Term Model of the Calculus of Constructions and Its Metamathematical Applications
- 5 Related Work, Extensions and Directions of Future Investigations
- Appendix Independence Proofs by Realizability Models
- References