A bittersweet announcement: I am pleased to announce that, together with my co-authors Edwin Brady (of St Andrews) & Guillaume Allais (soon to be of Strathclyde), we have a paper accepted to the Eelco Visser Commemorative Symposium 2023.
The work argues how we can link dependently-typed languages with language work benches, and highlights many of the techniques that Guillaume and I use when formally mechanising language’s in Idris2/Agda. The abstract is below:
Language Workbenches offer language designers an expressive environment in which to create theirDomain Specific Languages (DSLs). Similarly, research into mechanised meta-theory has shownhow dependently-typed languages provide expressive environments to formalise and study DSLs andtheir meta-theoretical properties. But can we claim that dependently-typed languages qualify as language workbenches? We argue yes!We have developed an exemplar DSL called Vélo that showcases not only dependently-typedtechniques to realise and manipulate Intermediate Representations (IRs), but that dependently-typedlanguages make fine language workbenches. Vélo is a simple verified language with well-typed holesand comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compilerpasses. Specifically, we describe our design choices for well-typed IR design that includes supportfor well-typed holes, how Common Sub-Expression Elimination (CSE) is achieved in a well-typedsetting, and how the mechanised type-soundness proof for Vélo is the source of the evaluator.
The artifact is available online:
https://doi.org/10.5281/zenodo.7573031
The GitHub repo is: