ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020

Reference immutability is a type-based technique for controlling mutation that has been thoroughly studied in Java. We explore how reference immutability interacts with the features of Scala by adding it to the Dependent Object Types (DOT) calculus. Our extension shows how reference immutability can be encoded using existing Scala features such as path-dependent, intersection, and union types. We prove type soundness and the immutability guarantee provided by our calculus.