Intrinsically-Typed Language Composition: Go/No-Go
Cas van der Rest
Date: Wed, January 20, 2021
Room: Eelco's Zoom Room
Note: This is a PhD Go/No-Go meeting
Intrinsically-typed definitional interpreters are an attractive way to define languages, tightly integrating specification and proof. Although is is common to define the same constructs for different languages, copy-paste reuse is still the de-facto standard way of sharing code between such interpreters. A preferable approach would be to compose interpreters from separately-defined components.
Modern dependently-typed languages such as Agda, however, offer no built-in support for the composition of data types and functions, which are the core language features underlying intrinsically-typed definitional interpreters. In this project, the goal is to both define a model of intrinsically-typed language fragments and fragment composition, as well as to explore how such a model may help to develop better tools for language designers.
Artem Shinkarov | Extracting Agda-embedded DSLs
Next: Aron Zwaan | Composable Type System Specification using Heterogeneous Scope Graphs