Inline videos. See also:Category: Articles with embedded Videos..

System F

From Biocrawler, the free encyclopedia.

For the electronic dance music artist, see Ferry Corsten

System F is a typed lambda calculus. It is also known as the second-order or polymorphic lambda calculus. It was discovered independently by the logician Jean-Yves Girard and the computer scientist John C. Reynolds. System F formalizes the notion of parametric polymorphism in programming languages.

Just as the lambda calculus has variables ranging over functions, and binders for them, the second-order lambda calculus 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 judgement

$\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha$

where α is a type variable.

Under the Curry-Howard isomorphism, System F corresponds to a second-order logic.

System F, together with even more expressive lambda calculi, can be seen as part of the lambda cube.

This mathematics-related article is a stub. You can help Biocrawler by expanding it (http://www.biocrawler.com/w/index.php?title=System_F&action=edit).

[edit]