Mutable WadlerFest DOT
Marianna Rapoport, Ond\v{r}ej Lhot\'ak

TL;DR
This paper extends the Dependent Object Types calculus to include typed mutable reference cells, enabling modeling of mutation and effectful computation in Scala, with a formal proof of soundness.
Contribution
It introduces a typed mutation extension to DOT and provides a mechanized proof of its soundness in Coq, addressing a key gap in modeling Scala features.
Findings
Extension of DOT with typed mutable references
Mechanized proof of soundness in Coq
Enhanced modeling of Scala's mutation features
Abstract
The Dependent Object Types (DOT) calculus aims to model the essence of Scala, with a focus on abstract type members, path-dependent types, and subtyping. Other Scala features could be defined by translation to DOT. Mutation is a fundamental feature of Scala currently missing in DOT. Mutation in DOT is needed not only to model effectful computation and mutation in Scala programs, but even to precisely specify how Scala initializes immutable variables and fields (vals). We present an extension to DOT that adds typed mutable reference cells. We have proven the extension sound with a mechanized proof in Coq. We present the key features of our extended calculus and its soundness proof, and discuss the challenges that we encountered in our search for a sound design and the alternative solutions that we considered.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Distributed systems and fault tolerance · Security and Verification in Computing
