Grokking the Sequent Calculus (Functional Pearl)

by David Binder, Marco Tzschentke, Marius Müller, and Klaus Ostermann

In Proc. Int’l Conf. Functional Programming (ICFP). ACM Press, 2024.

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.

Citation as BibTeX

@inproceedings{binder24grokking,
  author = {Binder, David and Tzschentke, Marco and Müller, Marius and Ostermann, Klaus},
  title = {Grokking the Sequent Calculus (Functional Pearl)},
  booktitle = {Proc. Int’l Conf. Functional Programming (ICFP)},
  year = {2024},
  publisher = {ACM Press},
  doi = {10.1145/3674639}
}