2024/06/20 by David Binder, David A. Binder, Marco Tzschentke +2 · 2 voices · 1 citation
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Computability, Logic, AI Algorithms
paper · pdf · doi:10.1145/3674639
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.