  Scala's type system unifies ML modules, object-oriented, and functional
programming. The Dependent Object Types (DOT) family of calculi has been
proposed as a new foundation for Scala and similar languages. Unfortunately, it
is not clear how DOT relates to any well-known type systems, and type soundness
has only been established for very restricted subsets. In fact, important Scala
features are known to break at least one key metatheoretic property such as
environment narrowing or subtyping transitivity, which are usually required for
a type soundness proof.
  First, and, perhaps surprisingly, we show how rich DOT calculi can still be
proved sound. The key insight is that narrowing and subtyping transitivity only
need to hold for runtime objects, but not for code that is never executed.
Alas, the dominant method of proving type soundness, Wright and Felleisen's
syntactic approach, is based on term rewriting, which does not a priori make a
distinction between runtime and type assignment time.
  Second, we demonstrate how type soundness can be proved for advanced,
polymorphic, type systems with respect to high-level, definitional
interpreters, implemented in Coq. We present the first mechanized soundness
proof in this style for System F<: and several extensions, including mutable
references. Our proofs use only simple induction: another surprising result, as
the combination of big-step semantics, mutable references, and polymorphism is
commonly believed to require co-inductive proof techniques.
  Third, we show how DOT-like calculi emerge as generalizations of F<:,
exposing a rich design space of calculi with path-dependent types which we
collectively call System D. Armed with insights from the definitional
interpreter semantics, we also show how equivalent small-step semantics and
soundness proofs in Wright-Felleisen-style can be derived for these systems.
