Advertisement

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

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

Abstract

The aim of this chapter is to construct a doctrine of constructions C I as a term model of the Calculus of Constructions such that the interpretation in this model interprets only provably well-defined contexts, types and objects and identifies only those contexts, types or objects which are provably equal up to renaming of variables bound in the contexts.

Preview

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