Erweiterte
Suche ›

Semantics of Type Theory

Correctness, Completeness and Independence Results

Birkhäuser Boston,
Buch
96,29 € Lieferbar in 5-7 Tagen

Kurzbeschreibung

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.

Details
Schlagworte

Titel: Semantics of Type Theory
Autoren/Herausgeber: Thomas Streicher
Aus der Reihe: Progress in Theoretical Computer Science
Ausgabe: Softcover reprint of the original 1st ed. 1991

ISBN/EAN: 9781461267577

Seitenzahl: 299
Format: 23,5 x 15,5 cm
Produktform: Taschenbuch/Softcover
Gewicht: 486 g
Sprache: Englisch

buchhandel.de - Newsletter
Möchten Sie sich für den Newsletter anmelden?


Bitte geben Sie eine gültige E-Mail-Adresse ein.
Lieber nicht