The DOT calculus proposes a new type-theoretic foundation for languages like Scala. See the master branch for current developments on DOT.

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 updated model has been implemented in Coq, Dafny and PLT Redex.