Joint work with Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, Peter Mosses.
The code in this repository is associated with the paper Intrinsically-Typed Definitional Interpreters à la Carte, published at OOPSLA 2022. The paper, its accompanying artifact, and this repository are distributed under a CC-BY 4.0 license.
Browse the code interacively here
Familiar with Agda? Everything.agda imports all definitions.
Run make in the top level directory of this repository to check Everything.agda (which imports all definitions).
Run make doc in the top level directory of this repository to generate HTML documentation in docs/.
To view the code in the interactive and clickable format, open docs/Everything.html in your browser after generating the HTML.
Try
git submodule init
git submodule update --recursive
if building fails due to missing dependencies.