  The calculus of Dependent Object Types (DOT) has enabled a more principled
and robust implementation of Scala, but its support for type-level computation
has proven insufficient. As a remedy, we propose $F^\omega_{..}$, a rigorous
theoretical foundation for Scala's higher-kinded types. $F^\omega_{..}$ extends
$F^\omega_{<:}$ with interval kinds, which afford a unified treatment of
important type- and kind-level abstraction mechanisms found in Scala, such as
bounded quantification, bounded operator abstractions, translucent type
definitions and first-class subtyping constraints. The result is a flexible and
general theory of higher-order subtyping. We prove type and kind safety of
$F^\omega_{..}$, as well as weak normalization of types and undecidability of
subtyping. All our proofs are mechanized in Agda using a fully syntactic
approach based on hereditary substitution.
