A Path to DOT: Formalizing Scala with Dependent Object Types

Abstract

The goal of my thesis is to enable formal reasoning about the Scala programming language. To that end I present a core calculus that formalizes Scala's i) essential features in a ii) type-safe way and is iii) easy to extend with more features. I build on the Dependent Object Types (DOT) calculus that formalizes path-dependent types. My contributions are i) a generalization of DOT with types that depend on paths of arbitrary length, ii) a simple, extensible type-safety proof for DOT, and iii) an extension of DOT with mutable references. The simple proof makes designing smaller extensions such as mutation straightforward, and larger extensions, such as full support for paths, approachable. Adding fully path-dependent types to DOT allows us to model the key feature of Scala's type and module system. The calculi and proofs presented in my thesis are fully mechanized in Coq.