ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy

Bahr and Hutton recently developed an approach to compiler calculation that allows a wide range of compilers to be derived from specifications of their correctness. However, a limitation of the approach is that it results in compilers that produce tree-structured code. By contrast, realistic compilers produce code that is essentially graph-structured, where the edges in the graph represent jumps that transfer the flow of control to other locations in the code. In the paper, we show how their approach can naturally be adapted to calculate compilers that produce graph-structured code, without changing the underlying calculational methodology, by using a higher-order abstract syntax representation of graphs. This artifact consists of an Agda formalisation of all calculations in the paper.