Two motivations led to the invention of the polymorphic lambda calculus (second order typed lambda calculus/System F). Girard [1971] invented it to extend the Curry-Howard correspondence to intuitionistic propositional logic with quantifiers. Reynolds [1974] independently reinvented it to permit the definition of "polymorphic" procedures in a typed programming language.

The polymorphic lambda calculus allows impredicative definitions. For example, the type an expression of type "forall t.t->t" can be applied to the same type "forall t.t->t". However, we do have strong beta-normalization. (Girard showed weak beta-normalization and Prawitz showed strong beta-normalization.) This implies cut-elimination for the intuitionistic propositional calculus with quantifiers. Computationally, this implies that terms describe terminating procedures. Thus, the set of functions representable as terms in the polymorphic lambda-calculus (without a recursion operator) does not exhaust the recursive functions. However, Girard showed every function from the naturals to the naturals that can be proven total using second-order arithmetic can be expressed as such a term. This includes p.r. functions and Ackermann's function.

The natural numbers are represented using Church's numerals (except type variable bindings allow us to have a single term "n"--as opposed to an "n" for each type). Church's numerals in the polymorphic lambda calculus have type "forall t.(t->t)->(t->t)." The numeral "n" is the term "Lambda t.lambda f:t->t.lambda x:t.f(f(...f(x)...))" where f is applied n times. Considering all the possible (intuitionistic) proofs of "forall t.(t->t)->(t->t)" we are led to the conclusion that every closed term of type "forall t.(t->t)->(t->t)" beta-reduces to a Church numeral. So, the type "forall t.(t->t)->(t->t)" can be used to define the type "nat."

The type "bool" can be defined by "forall t.t->(t->t)" which has two closed beta-normal forms: "Lambda t.lambda x:t,y:t.x" and "Lambda t.lambda x:t,y:t.y." The type list(s) (where s is a type) can be defined by "forall t.(s->(t->t))->(t->t)" which has closed beta-normal forms "Lambda t.lambda f:s->(t->t),x:t.f(e1)(...(f(en)(x))...)" where each ei is a closed beta-normal form of type s. More generally, Bohm and Leivant proved "for any many-sorted algebraic signature (without laws), there is a set of polymorphic types (one for each sort) whose closed normal forms constitute an initial algebra."

There are two types of models: PER models interpret types as sets of (equivalence classes of) partial equivalence relations on a model of the untyped lambda calculus; domain-based models interpret types as Scott domains [cpo's]. The domain-based models permit the addition of fixed point operators to the language (and hence cannot capture the fact that reduction of all terms terminate). Also, the type "forall t.t" (which should intuitively be empty) denotes a nonempty domain. The domain-based models also fail to capture parametricity. It was not known if any PER models capture parametricity, but since the paper was written, Bainbridge, Freyd, Scedrov and Scott showed how to construct a parametric PER model. (See also the reports on the following page.)

There are no set-theoretic parametric models (that is, parametric models in which the exponent type "a->b" is interpreted as the full set-theoretic function space B^A).