Back to Search
Start Over
Semantics of Type Theory : Correctness, Completeness and Independence Results
- Publication Year :
- 2012
-
Abstract
- 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.
- Subjects :
- Mathematics—Data processing
Computer science—Mathematics
Subjects
Details
- Language :
- English
- ISBNs :
- 9780817635947, 9781461267577, and 9781461204336
- Database :
- eBook Index
- Journal :
- Semantics of Type Theory : Correctness, Completeness and Independence Results
- Publication Type :
- eBook
- Accession number :
- 2816316