Models for the Calculus of Constructions and Its Extensions

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


E. Moggi [Mo] (for a recent paper version of Moggi’s original ideas see [LoMo]) has introduced for any partial combinatory algebra D, see e.g. [Be], the category D-Set of D-sets and realizable morphisms between D-sets as a structure where to define a model for the polymorphic λ-calculus by using the D-set of all partial equivalence relations on D as the type of propositions. E. Moggi’s ideas are based on previous work on a topos-theoretic account of Kleene’s notion of realisability following suggestions of Dana Scott and developed to a considerable amount by the group around M. Hyland and A. Pitts in Cambridge, see e.g. [Hy].


Categorical Model Full Subcategory High Order Logic Contextual Category Partial Recursive Function 
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