Type safety for core Scala – based on Definitional Interpreters (lambda-the-ultimate.org)

The first formal type system that works for (simplified) Scala.

More generally, shifting from term rewriting to operational semantics (i.e. proving interpreters correct) seems like a big improvement. Instead of working in a completely different semantic domain, we work in one closely allied to our implementations.

As the post says at the bottom, this solves a problem that has been open for over a decade.

Also! I did not know that Odersky & associates are working on a clean reimplementation of Scala called "Dotty" that is named after exactly this kind of type theory (Dependent Object Types or DOT).

They just got their compiler to self-host, see https://github.com/lampepfl/dotty and http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-boo...