Write a Blog >>
Tue 20 Jun 2017 14:55 - 15:30 at Vertex WS217 - C Chair(s): Martin Berger

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 (\textsf{val}s).

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.

Conference Day
Tue 20 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
14:00
20m
Talk
Generic Approach to Certified Static Checking of Module-like Constructs
FTfJP
Julia BelyakovaSouthern Federal University
Pre-print
14:20
35m
Talk
Tracing sharing in an imperative pure calculus
FTfJP
Paola GianniniUniversita' del Piemonte Orientale, Marco ServettoVictoria University of Wellington, Elena ZuccaUniversity of Genova
14:55
35m
Talk
Mutable WadlerFest DOT
FTfJP
Marianna RapoportUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo, Canada