Semantics of Type Theory pp 112-155 | Cite as

# Models for the Calculus of Constructions and Its Extensions

## Abstract

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].

## Keywords

Categorical Model Full Subcategory High Order Logic Contextual Category Partial Recursive Function## Preview

Unable to display preview. Download preview PDF.