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 theory
Mathematical Proceedings of the Cambridge Philosophical Society, 1984
Semantics for classical AUTOMATH and related systems
Information and Control, 1983
HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
Mathematical Logic Quarterly, 1983
Tripos theory
Mathematical Proceedings of the Cambridge Philosophical Society, 1980
The „Dialectica”︁ Interpretation and Categories
Mathematical Logic Quarterly, 1978
Abstract families and the adjoint functor theorems
Published by Springer Nature ,1978
Data Types as Lattices
SIAM Journal on Computing, 1976
Ouelques Resultats sur les Interpretations Fonctionnelles
Published by Springer Nature ,1973
Aspects of topoi
Bulletin of the Australian Mathematical Society, 1972