Composable, safe-by-construction interpreters for typed languages

Cas van der Rest

Date: Wed, March 11, 2020
Time: 12:00

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 |
Next: Hendrik van Antwerpen |