一句话：提出 gDOT 演算，并用 Iris 中的步进索引逻辑关系模型在 Coq 中机器化证明了其可靠性。
论文关注 Scala 核心类型系统 DOT（依赖对象类型）的元理论难以扩展、若干重要特性的可靠性长期悬而未决的问题。作者采用语义优先的路线，为 DOT 的新变体 guarded DOT（gDOT）建立了逻辑关系模型，借助 Iris 框架提供的抽象步进索引（step-indexing）刻画 gDOT 中的多种递归形式。他们用该模型证明 gDOT 具备所期望的数据抽象性质，并给出先前 DOT 版本无法处理的 Scala 实例，以说明 gDOT 的表达力。gDOT 的类型系统、语义模型、可靠性证明以及论文中的全部示例均已在 Coq 中机器化验证。
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.
@article{GiarrussoSTBK20,
title = {Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris},
author = {Paolo G. Giarrusso and Léo Stefanesco and Amin Timany and Lars Birkedal and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408996}
}