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.
Why are you interested in it or why should it be a good idea?
Grokking the Sequent Calculus (Functional Pearl) David Binder, Marco Tzschentke, Marius MΓΌller, Klaus Ostermann ICFP 2024
PDF
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.
Why are you interested in it or why should it be a good idea?
@tpetricek