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.