Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10118865 | Annals of Pure and Applied Logic | 2005 | 47 Pages |
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.
Keywords
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Samson Abramsky, Marina Lenisa,