Linear realizability and full completeness for typed lambda-calculi

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.