Scala step-by-step

Scala step-by-step: Soundness for DOT with step-indexed logical relations in Iris

Giarrusso, P.G. (TU Delft Programming Languages)
Stefanesco, Leo (Université de Paris)
Timany, Amin (Aarhus University)
Birkedal, Lars (Aarhus University)
Krebbers, R.J. (TU Delft Programming Languages)

2020

The metatheory of Scala's core type system - the Dependent Object Types (DOT) calculus - is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and in practice. To address some of these problems, we use a semantics-first approach to develop a logical relations model for a new version of DOT, called guarded DOT (gDOT). Our logical relations model makes use of an abstract form of step-indexing, as supported by the Iris framework, to model various forms of recursion in gDOT. To demonstrate the expressiveness of gDOT, we show that it handles Scala examples that could not be handled by previous versions of DOT, and prove using our logical relations model that gDOT provides the desired data abstraction. The gDOT type system, its semantic model, its soundness proofs, and all examples in the paper have been mechanized in Coq.

Coq
data abstraction
DOT
Iris
logical relations
Scala
step-indexing
type soundness

http://resolver.tudelft.nl/uuid:b2942dd8-e6ac-4568-9208-9dbfc20a2a8a

https://doi.org/10.1145/3408996

2475-1421

Proceedings of the ACM on Programming Languages, 4 (ICFP), 114:1 - 114:29

Institutional Repository

journal article

© 2020 P.G. Giarrusso, Leo Stefanesco, Amin Timany, Lars Birkedal, R.J. Krebbers