Higher-Order Subtyping

Martin Steffen and Benjamin Pierce

Abstract: System F omega sub is an extension with subtyping of Girard's higher-order polymorphic lambda-calculus. We develop the fundamental metatheory of this calculus: decidability of beta-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.

LFCS report ECS-LFCS-94-280, February 1994.

Previous | Index | Next