5 ms·
Type safety for core Scala – based on Definitional Interpreters
- jedharris 11y agoThe 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.
- jedharris 11y agoAs the post says at the bottom, this solves a problem that has been open for over a decade.
- jedharris 11y agoAlso! 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 https://github.com/lampepfl/dotty and http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-bootstraps.html http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-boo...