UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

A Path to DOT: Formalizing Scala with Dependent Object Types

Thumbnail Image

Files

Rapoport_Marianna.pdf (875.21 KB)

Date

2019-12-13

Authors

Rapoport, Marianna

Journal Title

Journal ISSN

Volume Title

Publisher

University of Waterloo

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.

Description

Keywords

Coq, DOT, programming languages, Scala, type safety, type systems

LC Keywords

Citation

URI

http://hdl.handle.net/10012/15322

Collections

Theses
Computer Science