PhD Defence • Programming Languages — A Path to DOT: Formalizing Scala with Dependent Object Types

Marianna Rapoport, PhD candidate
David R. Cheriton School of Computer Science

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 

• essential features in a
• type-safe way and is
• easy to extend with more features.

I build on the Dependent Object Types (DOT) calculus that formalizes path-dependent types. My contributions are

• a generalization of DOT with types that depend on paths of arbitrary length,
• a simple, extensible type-safety proof for DOT, and
• 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.