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.

翻译：依赖对象类型（DOT）演算旨在为Scala语言奠定坚实的形式化基础，然而DOT基于结构子类型，而Scala本质上是一种基于类的语言。这种阻抗不匹配意味着仅凭DOT的可靠性证明并不足以声明语言特定子集的可靠性。尽管已有少量Scala代码片段被手动翻译为DOT，但至今尚未提出系统性的编译方案。本论文开发了一系列复杂度递增的演算来建模Scala语言，并为每个演算提出了一个类型保持的编译方案，将其编译为DOT。在此过程中，我们还为DOT开发了一些必要的扩展。