System F is a kind of typed lambda calculus that introduces universal quantification of types.
Girard under the name System F and by Reynolds under the name polymorphic typed λ-calculus
Girard wanted to design a language with termination guarantee but still be able to encode all kinds of types.
Types
Where the syntax
Expressions
Note that
Two Forms of Judgement
Where
Typing Rule
Arrow:
For all is very much like arrow:
Application
Abstraction
Type Application
Type Abstraction