Categorical semantics for higher order polymorphic lambda calculus

DOI10.2307/2273831zbMATH Open0642.03007OpenAlexW2032017843MaRDI QIDQ3783264FDOQ3783264

Authors: 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

Recommendations

• scientific article; zbMATH DE number 4027427
• scientific article; zbMATH DE number 4027428
• scientific article; zbMATH DE number 937388
• Categorical abstract machines for higher-order typed \(\lambda\)-calculi
• scientific article
• Categorical models for a semantically linear \(\lambda\)-calculus
• scientific article; zbMATH DE number 3882403
• scientific article; zbMATH DE number 4047683
• Decomposing typed lambda calculus into a couple of categorical programming languages
• scientific article; zbMATH DE number 3999254

zbMATH Keywords

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Tripos theory
• Title not available (Why is that?)
• Data Types as Lattices
• Locally cartesian closed categories and type theory
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Aspects of topoi
• Semantics for classical AUTOMATH and related systems
• The „Dialectica”︁ Interpretation and Categories
• Title not available (Why is that?)

Cited In (52)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3783264)