一句话：提出以相继式演算贯穿全程的编译器，支持控制效应与 data/codata 混合求值，可生成机器码。
将高层函数式语言高效编译到现代机器码需跨越众多抽象层次，若语言包含控制效应并混合求值策略（如按值 data 与按名 codata）则更难。论文完整讲述从带控制效应、同时含 data 与 codata 的简单函数式语言到标准平台机器码的编译过程。与现有函数式编译器不同，其所有中间阶段均采用受相继式演算启发的语言，这类语言以消费者（表示程序上下文）为一等公民。作者将该工作视为 Appel“Compiling with Continuations”的延续与泛化，展示了一条统一的编译路径。摘要未给出量化评估，但表明可生成标准平台机器码。
Compiling a high-level functional programming language to machine code that can be executed efficiently on a modern machine is complicated, since we have to traverse many different levels of abstraction. This is particularly challenging if the language contains some form of control effects and a mix of different evaluation strategies, such as call-by-value data types and call-by-name codata types. In this paper, we tell the complete story, starting from a simple functional programming language with control effects and both data and codata types, and ending up with machine code for standard platforms. What distinguishes our compiler from all other existing compilers for functional programming languages is that, instead of natural-deduction-based languages like the lambda calculus, we use sequent-calculus-inspired languages throughout all intermediate stages. These sequent-calculus-based languages are characterized by the first-class nature of consumers, which represent program contexts. In this sense, we view our work as a continuation, and generalization, of Andrew Appel's landmark work on “Compiling with Continuations”.
DOI 原文 ·
@inproceedings{paperbot3945,
title = {Compiling with the Sequent Calculus},
author = {Marius Müller and David Binder and Marco Tzschentke and Philipp Schuster and Klaus Ostermann and Jonathan Immanuel Brachthäuser},
booktitle = {TOPLAS},
year = {2026},
doi = {10.1145/3845991}
}