一句话：本文通过实现一个到 λμμ˜-演算的编译器，首次面向编译器开发者介绍相继式演算作为中间语言。
相继式演算常被视为自然演绎的对称替代，但其项赋值系统 λμμ˜-演算主要面向类型论与逻辑学家，编译器开发者难以领略其价值。本文是一篇面向编译器开发者和编程语言爱好者的函数式珍珠，首次以非类型论专家的视角介绍 λμμ˜-演算。作者实现一个从一个小而有趣的表面语言到 λμμ˜-演算的编译器，并把后者用作编译器中间语言，借此展示其对求值上下文的一等表示等特性。文章以教学和示例驱动为主，旨在降低入门门槛，使读者理解相继式演算为何适合作为编译器 IR，而非报告新的类型规则或实证性能评估。
The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The λμμ˜-calculus is a term assignment system for the sequent calculus and a great foundation for compiler intermediate languages due to its first-class representation of evaluation contexts. Unfortunately, only experts of the sequent calculus can appreciate its beauty. To remedy this, we present the first introduction to the λμμ˜-calculus which is not directed at type theorists or logicians but at compiler hackers and programming-language enthusiasts. We do this by writing a compiler from a small but interesting surface language to the λμμ˜-calculus as a compiler intermediate language.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2406-14719,
title = {Grokking the Sequent Calculus (Functional Pearl)},
author = {David Binder and Marco Tzschentke and Marius Müller and Klaus Ostermann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674639}
}