一句话：为 CPS 演算建立可靠归约语义与简单类型强规范化证明，奠定编译器 IR 的形式理论基础。
编译器常通过 CPS 变换产生一类函数不再返回的中间表示语言，但这类 IR 缺乏统一的操作理论。本文研究 Thielecke 的 CPS-calculus，并扩展出可靠归约语义，以忠实刻画实际编译器中的优化规则；随后按 Plotkin 的思路证明它可作为 Appel 与 Kennedy 编译器 IR 的理论基础。文章还证明简单类型下 CPS-calculus 强规范化，采用一种新的“远距离可归约性”证明方法，并由此推出逻辑一致性。这些结果填补了现有文献空白，为 IR 的形式化推理提供理论工具。
The continuation-passing style translation often employed by compilers gives rise to a class of intermediate representation languages where functions are not allowed to return anymore. Though the primary use of these intermediate representation languages is to expose details about a program’s control flow, they may be equipped with an equational theory in order to be seen as specialized calculi, which in turn may be related to the original languages by means of a factorization theorem. In this paper, we explore Thielecke’s CPS-calculus, a small theory of continuations inspired by compiler implementations, and study its metatheory. We extend it with a sound reduction semantics that faithfully represents optimization rules used in actual compilers, and prove that it acts as a suitable theoretical foundation for the intermediate representation of Appel’s and Kennedy’s compilers by following the guidelines set out by Plotkin. Finally, we prove that the CPS-calculus is strongly normalizing in the simply typed setting by using a novel proof method for reasoning about reducibility at a distance, from which logical consistency follows. Taken together, these results close a gap in the existing literature, providing a formal theory for reasoning about intermediate representations.
@article{TorrensOV24,
title = {On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs},
author = {Paulo Torrens and Dominic Orchard and Cristiano Vasconcellos},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674630}
}