Dependent Object Types (DOT)

The DOT calculus proposes a new foundation for Scala's type system.

DOT has been presented at the FOOL 2012 workshop (PDF). The FOOL model has been implemented in Coq, PLT Redex, and Scala.

Since the FOOL presentation, we've been revising the formal model (PDF), in preparation for a mechanized type safety proof. The current model has been implemented in Coq, Dafny and PLT Redex.