A Path To DOT: Formalizing Fully Path-Dependent Types

Marianna Rapoport, Ondřej Lhoták

The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on path-dependent types $-$ types such as $x.a_1\dots a_n.T$ that depend on…