A characterization of lambda definability in categorical models of implicit polymorphism

DOI10.1016/0304-3975(94)00283-OzbMath0873.68015OpenAlexW2034606068MaRDI QIDQ673121

Moez Alimohamed

Publication date: 28 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)00283-o

zbMATH Keywords

ccc modelslambda definability

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (6)

Semantic analysis of normalisation by evaluation for typed lambda calculus ⋮ Relative full completeness for bicategorical Cartesian closed structure ⋮ A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators ⋮ Logical relations for monadic types ⋮ Type-directed specialization of polymorphism. ⋮ Prelogical relations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Kripke-style models for typed lambda calculus
• An intersection problem for finite automata
• Kripke logical relations and PCF
• Logical relations and the typed λ-calculus
• Categorical semantics for higher order polymorphic lambda calculus
• Categories for Types
• Parametricity and local variables
• A category-theoretic account of program modules
• Types, abstraction, and parametric polymorphism, part 2

This page was built for publication: A characterization of lambda definability in categorical models of implicit polymorphism