From F to DOT: Type Soundness Proofs with Definitional Interpreters

A formal type system that works for 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.

Paper is here[1]

[1] http://arxiv.org/pdf/1510.05216v1