| Semantics of Type Theory: Correctness, Completeness and Independence Results Softcover Repri Edition Contributor(s): Streicher, T. (Author) |
|
 |
ISBN: 1461267579 ISBN-13: 9781461267577 Publisher: Birkhauser OUR PRICE: $94.99 Product Type: Paperback Published: October 2012 |
| Additional Information |
| BISAC Categories: - Mathematics | Counting & Numeration - Computers | Computer Science - Computers | Data Processing |
| Dewey: 004 |
| Series: Progress in Theoretical Computer Science |
| Physical Information: 0.66" H x 6.14" W x 9.21" (0.98 lbs) 299 pages |
| Descriptions, Reviews, Etc. |
| Publisher Description: 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. |