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

Monday, November 11, 2019 1:30 pm - 1:30 pm EST (GMT -05:00)

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,
  • 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.