System F ⩽ ω is an extension with subtyping of the higher-order polymorphic λ-calculus …
subtype relation, and the soundness, completeness, and termination of algorithms for subtyping …

… a calculus with higher-order subtyping and subkinding by … from a calculus of higher-order
subtyping to a subtyping-free … We have given a translation of a higher-order subtyping caJ…

… The contribution of this thesis is to weave together these two threads by com bining
higher-order subtyping, which forms the cornerstone of several recent mod els of typed object-…

… subtyping constraints. The result is a flexible and general theory of higher-order subtyping.
We … Whether or not their approach can be generalized to higher-order subtyping is a question …

… interconvertible types in the subtype relation. Therefore, our subtyping relation relates types
of a … procedure to check subtyping, we need a new presentation of the subtyping relation that …

… We survey previous work on higher-order subtyping, bounded polymorphism and translucent
type definitions in the second part of the chapter, and discuss how and where our work fits …

… The categorical semantics of higher-order inclusive subtypes is then generalized to a notion
… -order theory of subtypes as inclusions developed in Part I [25] to a higherorder context. The …

We relate standard techniques for solving recursive domain equations to previous models
with types interpreted as partial equivalence relations(per’s) over a Dm lambda model. This …

… To retain decidability also in the higher-order case, we adopt the Kernel Fun subtyping rule
for universal quantifiers, insisting on equal bounds for the two All-types under comparison: …

… subtyping for systems of higher-order subtyping with bounded quantification. Other proofs
have used reduction relations unrelated to the actual notion of computation of the type theory, …