Benjamin Pierce

TCS Journal 1998 Journal Article

Bounded existentials and minimal typing

• Giorgio Ghelli
• Benjamin Pierce

We study an extension of the second-order calculus of bounded quantification, System F ⩽, with bounded existential types. Surprisingly, the most natural formulation of this extension lacks the important minimal typing property of F ⩽, which ensures that the set of types possessed by a typeable term can be characterized by a single least element. We consider alternative formulations and give an algorithm computing minimal types for the slightly weaker Kernel Fun variant of F ⩽.

TCS Journal 1997 Journal Article

Corrigendum to “Higher-order subtyping” [Theoret. Comput. Sci. 176(1–2) (1997) 235–282]

• Benjamin Pierce
• Martin Steffen

TCS Journal 1997 Journal Article

Higher-order subtyping

• Benjamin Pierce
• Martin Steffen

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.