HIGHER-ORDER SUBTYPING

System F-less than or equal to(omega) is an extension with subtyping o f the higher-order polymorphic lambda-calculus - an orthogonal combina tion of Girard's system F-omega with Cardelli and Wegner's Kernel Fun variant of System F-less than or equal to. We develop the fundamental metatheory of this calculus: decidability of beta-conversion on well-k inded types, elimination of the ''cut-rule'' of transitivity from the subtype relation, and the soundness, completeness, and termination of algorithms for subtyping and typechecking.