Science Fair Project Encyclopedia
System F
- 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
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.
External links
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details