3 ms·
From F to DOT: Type Soundness Proofs with Definitional Interpreters
- virtualwhys 11y agoPaper is here[1] [1] http://arxiv.org/pdf/1510.05216v1 http://arxiv.org/pdf/1510.05216v1
- jedharris 11y agoA 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.