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.
200 University Avenue West
Waterloo, ON N2L 3G1