From F to DOT: Type Soundness Proofs with Definitional Interpreters

Tiark Rompf, Nada Amin

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 Sc…