Higher-order subtyping

System F ⩽ ω is an extension with subtyping of the higher-order polymorphic λ-calculus —an orthogonal combination of Girard's system F ω with Cardelli and Wegner's Kernel Fun variant of System F ⩽. We develop the fundamental metatheory of this calculus: decidability of β-conversion on well-kinded types, elimination of the “cut-rule” of transitivity from the subtype relation, and the soundness, completeness, and termination of algorithms for subtyping and typechecking.

Authors

• Benjamin Pierce
• Martin Steffen

Keywords

• Lambda-calculus
• Type systems
• Subtyping
• Polymorphism
• Bounded quantification
• Typechecking