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

Paolo G. Giarrusso, Leo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers

Research output: Contribution to journalArticleScientificpeer-review

1 Downloads (Pure)

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.

Original languageEnglish
Article number114
Pages (from-to)114:1 - 114:29
Number of pages29
JournalProceedings of the ACM on Programming Languages
Volume4
Issue numberICFP
DOIs
Publication statusPublished - 2020

Keywords

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

Fingerprint Dive into the research topics of 'Scala step-by-step: Soundness for DOT with step-indexed logical relations in Iris'. Together they form a unique fingerprint.

  • Cite this