Categorical Semantics for Higher Order Polymorphic Lambda Calculus
Seely, R. A. G.
J. Symbolic Logic, Tome 52 (1987) no. 1, p. 969-989 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
A categorical structure suitable for interpreting polymorphic lambda calculus (PLC) is defined, providing an algebraic semantics for PLC which is sound and complete. In fact, there is an equivalence between the theories and the categories. Also presented is a definitional extension of PLC including "subtypes", for example, equality subtypes, together with a construction providing models of the extended language, and a context for Girard's extension of the Dialectica interpretation.
Publié le : 1987-12-14
Classification:  
@article{1183742506,
     author = {Seely, R. A. G.},
     title = {Categorical Semantics for Higher Order Polymorphic Lambda Calculus},
     journal = {J. Symbolic Logic},
     volume = {52},
     number = {1},
     year = {1987},
     pages = { 969-989},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183742506}
}

Seely, R. A. G. Categorical Semantics for Higher Order Polymorphic Lambda Calculus. J. Symbolic Logic, Tome 52 (1987) no. 1, pp.  969-989. http://gdmltest.u-ga.fr/item/1183742506/