Composable, safe-by-construction interpreters for typed languages

Cas van der Rest

Using dependent types we can provide a comprehensive specification for many programming languages by writing a definitional interpreter, encoding the static semantics as invariants over our abstract syntax type. The benefit of this approach is that the semantics of the host language guarantees certain poperties we might care about, such as type soundness. The downside, however, is that these interpreters are monolithic in nature, and thus less practical for larger languages. We investigate how and when these definitional interpreters can be composed, drawing inspiration from existing solutions in the design space surrounding the expression problem.

---

Previous: Arjan Mooij | Reducing the Complexity of Industrial Legacy Software
Next: Hendrik van Antwerpen | Incremental Type Checkers using Scope Graphs