ιDOT: A DOT Calculus with Object Initialization
summary
Introduces iDOT, a DOT calculus that models Scala-style fields, strict field reads, and constructors and enforces initialization so null pointer exceptions cannot occur; it classifies objects as free and committed, uses a conceptual split heap to allow building mutually recursive graphs, translates from kDOT with added rules for uninitialized fields, and comes with a mechanized safety proof of about 10,000 lines of Coq (≈4,000 lines added over kDOT) demonstrating the Tree/Fruit examples.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:24Tracking Fruits!
- 1:59Path-dependent Types!
- 4:08Thinking Man Returns!
- 5:45Path-dependent Types are Sound
- 6:16Translation Problems for DOT/PDOT
- 8:11Overall Type and Initialization System
- 9:18Intuition for Proving Safety: Heap Splitting
- 9:40Creating Mutually Recursive Objects
- 10:42Heap Operations
- 11:02Assignment Operations
- 11:26Initialization type system
- 11:52Constructor Initialization
- 12:16Constructor Call Initialization Typing
related talks
49mFrom DOT to Dotty
37mThe DOT Calculus: An Introduction for Scala Programmers
42mDOT: Scala Types from Theory to Practice
01h 00mState of Dotty
29mTheoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
14mScala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
01h 39mHands-on Dotty
30mDotty and types: the story so far