One of the most distinguishing features of the Scala Programming Language is that it features path-dependent types. DOT calculi are a family of formalized programming languages that support path-dependent types. Proving type safety for a programming language with path-dependent types has proven difficult and after a long search Amin et al. presented a type safety proof of the WadlerFest DOT calculus. A more modular and extensible type safety proof for this calculus was later presented by Rapoport et al. This proof has been extended further to show various extensions of the WadlerFest DOT calculus are also sound.

While the proof of Rapoport et al. is simpler and modular than previous proofs, we believe there are more opportunities for simplification. In this talk, we will discuss additional simplifications that are possible for the DOT calculus. The Coq proofs associated with the material of this talk can be found at https://github.com/themaplelab/dot-public.