|
|
|
|
| LEADER |
03007nmm a2200325 u 4500 |
| 001 |
EB000618138 |
| 003 |
EBX01000000000000000471220 |
| 005 |
00000000000000.0 |
| 007 |
cr||||||||||||||||||||| |
| 008 |
140122 ||| eng |
| 020 |
|
|
|a 9781461204336
|
| 100 |
1 |
|
|a Streicher, T.
|
| 245 |
0 |
0 |
|a Semantics of Type Theory
|h Elektronische Ressource
|b Correctness, Completeness and Independence Results
|c by T. Streicher
|
| 250 |
|
|
|a 1st ed. 1991
|
| 260 |
|
|
|a Boston, MA
|b Birkhäuser
|c 1991, 1991
|
| 300 |
|
|
|a XII, 299 p
|b online resource
|
| 505 |
0 |
|
|a 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
|
| 653 |
|
|
|a Mathematics of Computing
|
| 653 |
|
|
|a Computer science / Mathematics
|
| 653 |
|
|
|a Computational Mathematics and Numerical Analysis
|
| 653 |
|
|
|a Mathematics / Data processing
|
| 653 |
|
|
|a Mathematical Applications in Computer Science
|
| 653 |
|
|
|a Computational Science and Engineering
|
| 041 |
0 |
7 |
|a eng
|2 ISO 639-2
|
| 989 |
|
|
|b SBA
|a Springer Book Archives -2004
|
| 490 |
0 |
|
|a Progress in Theoretical Computer Science
|
| 028 |
5 |
0 |
|a 10.1007/978-1-4612-0433-6
|
| 856 |
4 |
0 |
|u https://doi.org/10.1007/978-1-4612-0433-6?nosfx=y
|x Verlag
|3 Volltext
|
| 082 |
0 |
|
|a 003.3
|
| 520 |
|
|
|a 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
|