A type system by J-Y. Girard. Also known as Lambda-2 or the polymorphic lambda-calculus.
["Proofs and Types", J-Y. Girard, Cambridge U Press 1989].
(23 Nov 1994)