System F

System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974).

Whereas simply typed lambda calculus has variables ranging over functions, and binders for them, System F additionally has variables ranging over types, and binders for them. As an example, the fact that the identity function can have any type of the form A→ A would be formalized in System F as the judgment

where ${\displaystyle \alpha }$ is a type variable. The upper-case ${\displaystyle \Lambda }$ is traditionally used to denote type-level functions, as opposed to the lower-case ${\displaystyle \lambda }$ which is used for value-level functions. (The superscripted ${\displaystyle \alpha }$ means that the bound x is of type ${\displaystyle \alpha }$; the expression after the colon is the type of the lambda expression preceding it.)

...
Wikipedia