一句话：将编译器计算从树结构扩展到图结构，用高阶抽象语法表示图，从正确性规约推导生成图结构代码的编译器。
该论文针对编译器计算方法的局限：既有从正确性规约推导编译器的技术只能生成树结构代码，而现实编译器通常生成图结构代码，其中边表示跳转到其他控制位置。作者在不改变原有计算式方法论的前提下，将这种方法自然扩展到图结构代码的推导，核心是采用高阶抽象语法（HOAS）来表示图。论文以函数式珍珠形式展示，说明如何从正确性规约计算得到产生图结构代码的编译器，从而使编译器计算更贴近实际编译器的控制流与跳转结构。
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 this article, 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.
@article{BahrH24,
title = {Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)},
author = {Patrick Bahr and Graham Hutton},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674638}
}