Linear realizability and full completeness for typed lambda-calculi

Annals of Pure and Applied Logic 134 (2-3):122-168 (2005)
  Copy   BIBTEX

Abstract

We present the model construction technique called Linear Realizability. It consists in building a category of Partial Equivalence Relations over a Linear Combinatory Algebra. We illustrate how it can be used to provide models, which are fully complete for various typed λ-calculi. In particular, we focus on special Linear Combinatory Algebras of partial involutions, and we present PER models over them which are fully complete, inter alia, w.r.t. the following languages and theories: the fragment of System F consisting of ML-types, the maximal theory on the simply typed λ-calculus with finitely many ground constants, and the maximal theory on an infinitary version of this latter calculus

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Weak typed Böhm theorem on IMLL.Satoshi Matsuoka - 2007 - Annals of Pure and Applied Logic 145 (1):37-90.
Kripke-style models for typed lambda calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.
Constructive set theoretic models of typed combinatory logic.Andreas Knobel - 1993 - Journal of Symbolic Logic 58 (1):99-118.
A completeness result for the simply typed λμ-calculus.Karim Nour & Khelifa Saber - 2010 - Annals of Pure and Applied Logic 161 (1):109-118.
Models for the Lambek calculus.Mati Pentus - 1995 - Annals of Pure and Applied Logic 75 (1-2):179-213.
A general notion of realizability.Lars Birkedal - 2002 - Bulletin of Symbolic Logic 8 (2):266-282.
Totality in arena games.Pierre Clairambault & Russ Harmer - 2010 - Annals of Pure and Applied Logic 161 (5):673-689.
A Mixed λ-calculus.Marie-Renée Fleury & Myriam Quatrini - 2007 - Studia Logica 87 (2-3):269-294.

Analytics

Added to PP
2014-01-16

Downloads
29 (#638,782)

6 months
13 (#207,084)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Affine logic for constructive mathematics.Michael Shulman - 2022 - Bulletin of Symbolic Logic 28 (3):327-386.

Add more citations

References found in this work

Completeness, invariance and λ-definability.R. Statman - 1982 - Journal of Symbolic Logic 47 (1):17-26.
Λ-definable functionals andβη conversion.R. Statman - 1983 - Archive for Mathematical Logic 23 (1):21-26.

Add more references