一句话：提出基于经典相继式演算的中间表示，并展示其可直接翻译到常规硬件，给出了形式描述、实现与初步性能评估。
编译器中间表示需要在便于翻译高层语言与便于生成代码之间取得平衡。基于逻辑系统的中间表示通常更易翻译，并具备对优化有价值的元理论性质。经典相继式演算因对称处理数据与控制流而被视为有潜力的候选，但此前尚不清楚如何将其编译到机器码。本文提出一种基于经典相继式演算的中间表示，给出其到常规硬件的直接翻译的形式描述，并实现原型编译器，体现了编译的对偶性。初步性能评估表明该方案可行。
Compiler intermediate representations have to strike a balance between being high-level enough to allow for easy translation of surface languages into them and being low-level enough to make code generation easy. An intermediate representation based on a logical system typically has the former property and additionally satisfies several meta-theoretical properties which are valuable when optimizing code. Recently, classical sequent calculus, which is widely recognized and impactful within the fields of logic and proof theory, has been proposed as a natural candidate in this regard, due to its symmetric treatment of data and control flow. For such a language to be useful, however, it must eventually be compiled to machine code. In this paper, we introduce an intermediate representation that is based on classical sequent calculus and demonstrate that this language can be directly translated to conventional hardware. We provide both a formal description and an implementation. Preliminary performance evaluations indicate that our approach is viable.
@article{paperbot3173,
title = {Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation},
author = {Philipp Schuster and Marius Müller and Klaus Ostermann and Jonathan Immanuel Brachthäuser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720507}
}