Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
summary
Presents a semantics-first proof that adds guardedness to DOT via a step-indexed logical relation built in Iris, yielding gDOT that models impredicative abstract type members by inserting a later guard on stored types. The development is fully mechanized in Coq, proves data abstraction, handles Scala examples previous DOTs could not, and totals about 9,000 lines of soundness proofs plus 5,000 lines of examples.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:34Why study Scala and DOT?
- 1:39Scala's Open Problem: Type Soundness
- 2:11Our Approach: Semantics-first Design
- 3:31val solution = new type Validator
- 4:49Example Summary
- 5:46Logical relation models
- 6:58Types Members, Naively
- 7:58Type Members, Soundly with Iris
- 8:59Retrofitting DOT over Model: gDOT
- 9:53gDOT key typing rules
- 11:27Contributions/In the paper
- 12:03Future work
- 12:41Conclusions
related talks
49mFrom DOT to Dotty
14mιDOT: A DOT Calculus with Object Initialization
29mTheoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
42mDOT: Scala Types from Theory to Practice
37mThe DOT Calculus: An Introduction for Scala Programmers
01h 00mState of Dotty
01h 39mHands-on Dotty
01h 05mSemantic Intermediate Representations for Sound Language Interoperability