Categorical semantics for higher order polymorphic lambda calculus

DOI10.2307/2273831zbMath0642.03007OpenAlexW2032017843MaRDI QIDQ3783264

R. A. G. Seely

Publication date: 1987

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/23a40e57eb3092ecda7204eb5e397f4fb92fb440

zbMATH Keywords

subtypesGirard's extension of the Dialectica interpretationsemantics for polymorphic lambda calculus

Mathematics Subject Classification ID

Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Nonclassical models (Boolean-valued, sheaf, etc.) (03C90) Combinatory logic and lambda calculus (03B40)

Related Items (34)

\(F\)-semantics for type assignment systems ⋮ Categorical abstract machines for higher-order typed \(\lambda\)-calculi ⋮ Least fixpoints of endofunctors of cartesian closed categories ⋮ Categorical models for non-extensional λ-calculi and combinatory logic ⋮ Logical systems. I: Internal calculi. ⋮ Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus ⋮ Categorical data types in parametric polymorphism ⋮ Semantics of the second order lambda calculus ⋮ A category-theoretic account of program modules ⋮ On the semantics of second order lambda calculus: From bruce-meyer-mitchell models to hyperdoctrine models and vice-versa ⋮ A remark on the theory of semi-functors ⋮ An exper model for Quest ⋮ Types, abstraction, and parametric polymorphism, part 2 ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ Universal properties for universal types in bifibrational parametricity ⋮ On some connections between logic and category theory ⋮ Bifibrational functorial semantics of parametric polymorphism ⋮ A modest model of records, inheritance, and bounded quantification ⋮ Bunched polymorphism ⋮ Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes ⋮ A characterization of lambda definability in categorical models of implicit polymorphism ⋮ Categorical models of polymorphism ⋮ Second-order type isomorphisms through game semantics ⋮ A game semantics for generic polymorphism ⋮ Unnamed Item ⋮ Comprehensive Parametric Polymorphism: Categorical Models and Type Theory ⋮ Categories of embeddings ⋮ Extensional models for polymorphism ⋮ A category-theoretic account of program modules ⋮ Functorial polymorphism ⋮ Typed Applicative Structures and Normalization by Evaluation for System F ω ⋮ Unnamed Item ⋮ Classifying categories for partial equational logic ⋮ CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Locally cartesian closed categories and type theory
• Semantics for classical AUTOMATH and related systems
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Tripos theory
• Data Types as Lattices
• The „Dialectica”︁ Interpretation and Categories
• Aspects of topoi

This page was built for publication: Categorical semantics for higher order polymorphic lambda calculus