Dependent Object Types (DOT)

September 8, 2016 · View on GitHub

The DOT calculus proposes a new type-theoretic foundation for languages like Scala. The latest rules (PDF) are for a small-step storeless variant with full subtyping lattice, recursive types including their subtyping, and dependent method types. Here is the corresponding mechanized soundness proof.

From F to DOT in Small-Step:

F_<:
F_<:>
D_<:
D_<:>
D_<>
DOT

Historical development:

OOPSLA'16 (PDF, code)
WadlerFest'16 (PDF, code)
From F to DOT (PDF, code)
OOPSLA'14 (PDF, code)
FOOL'12 (PDF, code)