Aarhus University Seal / Aarhus Universitets segl

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

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperConference articleResearchpeer-review

Documents

  • 3408996

    Final published version, 445 KB, PDF document

DOI

  • Paolo G. Giarrusso, Delft University of Technology
  • ,
  • Léo Stefanesco, University of Paris
  • ,
  • Amin Timany
  • Lars Birkedal
  • Robbert Krebbers, Delft University of Technology

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.

Original languageEnglish
Article number114
JournalProceedings of the ACM on Programming Languages
Volume4
IssueICFP
Number of pages29
DOIs
Publication statusPublished - Aug 2020

    Research areas

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

See relations at Aarhus University Citationformats

ID: 196497428