The DOT Calculus is a formalization of the Scala programming language focusing on path-dependent types.
This repo collects a bunch of type safety proofs of the DOT calculus.
Some simplifications of the Rapoport et al. type safety proof are provided in dot-simpler folder.
The ιDOT calculus is a DOT Calculus which enforces a sound object initialization order using a type and effect system. The calculus and several of its extensions are provided in the idot folder.