This is the homepage for the guarded DOT project. We extend the the DOT calculus, that is, the formal foundations of the Scala programming language, using step-indexed logical relations and the Iris framework; the result is the guarded DOT(gDOT) calculus.

Our first paper, Scala Step-by-Step, corresponds to gDOT 1.0.

Publications

• Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris. Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal and Robbert Krebbers. ICFP 2020.

  Abstract: 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.

  • Official ACM Version
  • Author Version.
  • Extended Version. The appendix lists omitted typing rules.
  • Coq Formalization
  • Updated coqdoc.
  • Artifact: .
  • Original coqdoc.
  • ICFP 2020 talk: slides, and slides with transcript.

Trivia

• Q: Why “Scala Step-by-Step”?
• A: Because Scala is named after the Italian word for “staircase”. And because we use step-indexing.

News

• 2020-08-26: Added slides for ICFP’20 talk.
• 2020-08-01: Added extended version.
• 2020-08-01: Updated author version (with minor changes from camera-ready).
• 2020-07-05: Added link to artifact on Zenodo
• 2020-07-04: Author version online
• 2020-07-03: Website online
• 2014-06-24: AEC submission accepted.
• 2020-06-19: Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris unconditionally accepted at ICFP 2020.

Contacts

For any question or suggestion, feel free to contact me, Paolo G. Giarrusso, at p !dot! giarrusso (at) gmail !dot! com.