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 lambda-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 lambda-calculus with finitely many ground constants, and the maximal theory on an infinitary version of this latter calculus. Keywords: Typed lambda-calculi, ML-polymorphic types, linear logic, hyperdoctrines, PER models, Geometry of Interaction, (axiomatic) full completeness.