Intrinsically-Typed Interpreters for Linear Languages

Arjen Rouvoet

An intrinsically-typed definitional interpreter is an attractive way of specifying the dynamic semantics of a programming language. It is a concise specification that is executable and type safe by construction. Unfortunately, scaling up intrinsically-typed definitional interpreters to more complicated object languages often results in definitions that are cluttered with manual proof work. In linearly-typed languages (e.g., session-typed languages) one has to ensure that all values are used linearly, and that linearity is maintained throughout the definition of the interpreter.

We present new methods and tools that make it possible to implement intrinsically-typed definitional interpreters for linearly-typed languages in a way that hides the majority of the manual proof work. Inspired by separation logic, we develop reusable and composable abstractions for programming with linear operations using dependent types. We use these abstractions to define interpreters for linearly-typed lambda calculi with strong references, and concurrent, session-typed communication in Agda.

---

Previous: Dan Frumin | Compositional Non-Interference for Fine-Grained Concurrent Programs
Next: Reuben Rowe | Characterising renaming within OCaml’s module system