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 is variable binder.

Expressions

Note that and looks similar and their only difference is the kind of parameter (expression vs type)

Two Forms of Judgement

Where is a list of variable mapping to types (), and is a list of type variables.

Typing Rule

Arrow:

For all is very much like arrow:

Application

Abstraction

Type Application

Type Abstraction

References