A good proof is one that makes us wiser. -- Yuri Manin The DOT Calculus and its Variations Formalizations of the Dependent Object Types (DOT) calculus, from the bottom up, with soundness proofs at each step. From F to DOT: Type Soundness Proofs with Definitional Interpreters (POPL'17) [pdf] STLC F<: F<: Equivalence with Small-Step F<: with Mutable References F<: with Exceptions F<:> from the System D Square D<:> from the System D Square DOT in Big-Step older developments from 2015 Type Soundness for Dependent Object Types (OOPSLA'16) [pdf] DOT in small-step Foundations of Path-Dependent Types (OOPSLA'14) [pdf] muDOT