Grokking the Sequent Calculus (Functional Pearl)
David Binder, Marco Tzschentke, Marius Müller, Klaus Ostermann
TL;DR
The paper addresses the barrier to understanding the sequent calculus by presenting the $λμ̃μ$-calculus as a practical intermediate language and demonstrating it with a compiler from a small surface language to the calculus to expose evaluation contexts and control flow. It develops a concrete, stepwise translation from the surface language Fun to the sequent-calculus-based Core, covering arithmetic, binding forms, top-level definitions, algebraic data and codata, first-class functions, and control operators. It exposes deep dualities such as data versus codata and $μ$-abstraction versus $μ̃$-abstraction, and provides an interactive online evaluator to illustrate reductions and translations. The result is a usable bridge between sequent-calculus theory and practical compiler design, clarifying evaluation contexts and enabling targeted optimizations.
Abstract
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.