深入理解 Sequent Calculus（函数式珍珠）
Grokking the Sequent Calculus (Functional Pearl)
AI总结：
本文面向编译器黑客与编程语言爱好者，通过编写将小型表层语言转换为 λμμ-calculus 的编译器，首次以非逻辑学家的视角介绍了 sequent calculus 及其作为编译器中间语言的优势。
摘要：
sequent calculus（序列演算）是一种证明系统，被设计为自然演绎的更对称的替代方案。λμμ-calculus 是 sequent calculus 的项指派系统，并且由于其一流地表示了求值上下文，是编译器中间语言的绝佳基础。遗憾的是，只有 sequent calculus 的专家才能欣赏其美感。为了弥补这一点，我们提出了首个 λμμ-calculus 的介绍，它不是面向类型理论家或逻辑学家，而是面向编译器黑客和编程语言爱好者。我们通过编写一个编译器来实现这一点，该编译器将一种小而有趣的表层语言转换为 λμμ-calculus，作为编译器中间语言。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
