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)