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

  • Thomas Streicher
Part of the Progress in Theoretical Computer Science book series (PTCS)


According to Gerard Huet and Thierry Coquand the Calculus of Constructions is a typed λ-calculus where type expressions themselves can contain λ-expressions as subterms. The original presentation in [Col] is characterized by a lot of overloading which has puzzled many readers as there products of types, functional abstraction and universal quantification were represented by one and the same syntactic construct, namely [x:A]B. Another instance of overloading was their systematic mixing of two aspects of propositions, namely propositions as objects of type Prop and propositions as types. This ambiguity we avoid by the type-forming construct Proof, which when applied to an object p of type Prop gives the type Proof(p) of proofs of the proposition p.


Induction Hypothesis Type Expression Interpretation Function Equal Section Type Prop 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 1991

Authors and Affiliations

  • Thomas Streicher
    • 1
  1. 1.Fakultat für Mathematik und InformatikUniversität PassauPassauGermany

Personalised recommendations