Reference Mutability for DOT

Abstract:

Reference mutability is a type-based technique for controlling mutation that has been thoroughlystudied in Java. We explore how reference mutability interacts with the features of Scala by addingit to the Dependent Object Types (DOT) calculus. Our extension shows how reference mutabilitycan 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.

BibTeX:

@inproceedings{dort_reference_2020,
    title = {{Reference Mutability for DOT}},
    author = {Dort, Vlastimil and Lhoták, Ondřej},
    year = {2020},
    booktitle = {{Proceedings of 34th European Conference on Object-Oriented Programming}},
    publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
    series = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
    location = {Dagstuhl, Germany},
    doi = {10.4230/LIPIcs.ECOOP.2020.18},
    isbn = {978-3-95977-154-2},
    url = {https://drops.dagstuhl.de/opus/volltexte/2020/13175},
    volume = {166},
}

Proceedings paper