Categorical semantics for higher order polymorphic lambda calculus
- 1 December 1987
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 52 (4), 969-989
- https://doi.org/10.2307/2273831
Abstract
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.Keywords
This publication has 16 references indexed in Scilit:
- Introduction to Higher Order Categorical Logic.The Journal of Symbolic Logic, 1989
- Locally cartesian closed categories and type theoryMathematical Proceedings of the Cambridge Philosophical Society, 1984
- Semantics for classical AUTOMATH and related systemsInformation and Control, 1983
- HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITIONMathematical Logic Quarterly, 1983
- Tripos theoryMathematical Proceedings of the Cambridge Philosophical Society, 1980
- The „Dialectica”︁ Interpretation and CategoriesMathematical Logic Quarterly, 1978
- Abstract families and the adjoint functor theoremsPublished by Springer Science and Business Media LLC ,1978
- Data Types as LatticesSIAM Journal on Computing, 1976
- Ouelques Resultats sur les Interpretations FonctionnellesPublished by Springer Science and Business Media LLC ,1973
- Aspects of topoiBulletin of the Australian Mathematical Society, 1972