System F-sub

In the branch of mathematical logic known as type theory, System F_<:, pronounced "F-sub", is an extension of system F with subtyping. System F_<: has been of central importance to programming language theory since the 1980s^{[citation needed]} because the core of functional programming languages, like those in the ML family, support both parametric polymorphism and record subtyping, which can be expressed in System F_<:.

See also[]

• Bounded quantification
• POPLmark

References[]

• Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, Andre (1994). "An extension of system F with subtyping". Information and Computation, vol. 9. North Holland, Amsterdam. pp. 4–56. doi:10.1006/inco.1994.1013.
• Pierce, Benjamin (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8., Chapter 26: Bounded quantification

${\displaystyle \Gamma \vdash x:{\text{Int}}}$

This programming language theory or type theory-related article is a stub. You can help Wikipedia by .

• v
• t