κDOT: A DOT Calculus with Mutation and Constructors

Abstract

Scala is a functional and object-oriented programming language which unifies concepts from object and module systems by allowing for objects with type members which are referenced via path-dependent types. The Dependent Object Types (DOT) calculus of Amin et al. [2016] models only this core part of Scala, but does not have many fundamental features of Scala such as strict and mutable fields. Since the most commonly used field types in Scala are strict, the correspondence between DOT and Scala is too weak for us to meaningfully prove static analyses safe for Scala by proving them safe for DOT.

This thesis presents the κDOT calculus, a calculus in the DOT family which supports mutable fields and constructors. κDOT can emulate both lazy and strict fields, and the constructor calls in κDOT emulate how objects are created in Scala. We present the key features of κDOT, the key ideas required for type safety, and discuss how the operational semantics of κDOT relates to that of Scala.

κDOT is proven type safe via a mechanized proof in Coq.