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 preprint]
Type Soundness for Dependent Object Types (OOPSLA'16) [pdf]
Foundations of Path-Dependent Types (OOPSLA'14) [pdf]