The Dependent Object Type (DOT) calculus was designed to put Scala on a
sound basis, but while DOT relies on structural subtyping, Scala is a
fundamentally class-based language. This impedance mismatch means that a proof
of DOT soundness by itself is not enough to declare a particular subset of the
language as sound. While a few examples of Scala snippets have been manually
translated into DOT, no systematic compilation scheme has been presented so
far.

In this thesis we develop a series of calculi of increasing complexity
to model Scala and present a type-preserving compilation scheme from each of
these calculus into DOT. Along the way, we develop some necessary extensions
to DOT.