Progress in Theoretical Computer Science

Semantics of Type Theory

Correctness, Completeness and Independence Results

Authors: Streicher, Thomas

Buy this book

eBook $89.00
price for USA (gross)
  • ISBN 978-1-4612-0433-6
  • Digitally watermarked, DRM-free
  • Included format: PDF
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Softcover $119.00
price for USA
  • ISBN 978-1-4612-6757-7
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
About this book

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.

Table of contents (6 chapters)

  • Introduction

    Streicher, Thomas

    Pages 1-42

  • Contextual Categories and Categorical Semantics of Dependent Types

    Streicher, Thomas

    Pages 43-111

  • Models for the Calculus of Constructions and Its Extensions

    Streicher, Thomas

    Pages 112-155

  • Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions

    Streicher, Thomas

    Pages 156-220

  • The Term Model of the Calculus of Constructions and Its Metamathematical Applications

    Streicher, Thomas

    Pages 221-264

Buy this book

eBook $89.00
price for USA (gross)
  • ISBN 978-1-4612-0433-6
  • Digitally watermarked, DRM-free
  • Included format: PDF
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Softcover $119.00
price for USA
  • ISBN 978-1-4612-6757-7
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
Loading...

Recommended for you

Loading...

Bibliographic Information

Bibliographic Information
Book Title
Semantics of Type Theory
Book Subtitle
Correctness, Completeness and Independence Results
Authors
Series Title
Progress in Theoretical Computer Science
Copyright
1991
Publisher
Birkhäuser Basel
Copyright Holder
Springer Science+Business Media New York
eBook ISBN
978-1-4612-0433-6
DOI
10.1007/978-1-4612-0433-6
Softcover ISBN
978-1-4612-6757-7
Edition Number
1
Number of Pages
XII, 299
Topics