Related Work, Extensions and Directions of Further Investigations

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


In the previous chapters we have studied the Calculus of Constructions following a classical pattern. We have introduced a class of structures called doctrines of constructions in Chapter 1 and studied several instances of this notion in Chapter 2 (realizability and retract models). In Chapter 3 we have defined an axiomatization of the calculus and the interpretation of this calculus in arbitrary doctrines of constructions and then have proved a correctness theorem. Finally in Chapter 4 we have shown the existence of a term model. Further we have shown that only provably correct types and objects get an interpretation in the term model and only those equality judgments which can be derived in the calculus are valid under interpretation in the term model.


Identity Type Dependent Type Unique Section Chapter Versus Unique Morphism 
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