Models for the Calculus of Constructions and Its Extensions
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].
KeywordsCategorical Model Full Subcategory High Order Logic Contextual Category Partial Recursive Function
Unable to display preview. Download preview PDF.