Intrinsically-Typed Language Composition: Go/No-Go

Cas van der Rest


Date: Wed, January 20, 2021
Time: 12:15
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.

Previous: Artem Shinkarov |
Next: |