Linear realizability and full completeness for typed lambda-calculi
From MaRDI portal
Publication:556821
DOI10.1016/j.apal.2004.08.003zbMath1064.03012OpenAlexW1983399101WikidataQ57006682 ScholiaQ57006682MaRDI QIDQ556821
Marina Lenisa, Samson Abramsky
Publication date: 23 June 2005
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2004.08.003
(Axiomatic) Full completenessGeometry of InteractionHyperdoctrinesLinear logicML-polymorphic typesPER modelsTyped lambda-calculi
Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)
Related Items (8)
AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS ⋮ Semantics of higher-order quantum computation via geometry of interaction ⋮ Parallelism in realizability models ⋮ Coherence Spaces and Uniform Continuity ⋮ A type assignment system for game semantics ⋮ Generalized bounded linear logic and its categorical semantics ⋮ lambda!-calculus, Intersection Types, and Involutions ⋮ A structural approach to reversible computation
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Equational theories for inductive types
- Extensional models for polymorphism
- The lambda calculus. Its syntax and semantics. Rev. ed.
- New foundations for the geometry of interaction
- On full abstraction for PCF: I, II and III
- Full abstraction for PCF
- λ-definable functionals andβη conversion
- Completeness, invariance and λ-definability
- Categories for Types
- Games and full completeness for multiplicative linear logic
- Decidability of all minimal models
- Geometry of Interaction and linear combinatory algebras
- Traced monoidal categories
- Algebraic types in PER models
- Retracing some paths in process algebra
This page was built for publication: Linear realizability and full completeness for typed lambda-calculi
