Grokking the Sequent Calculus (Functional Pearl)

TL;DR

This paper introduces an accessible explanation of the { extlambda}{ extmu}{ extmu}-calculus, a proof system for the sequent calculus, by implementing a compiler from a surface language to this calculus, making it more approachable for programmers.

Contribution

It provides the first non-technical introduction to the { extlambda}{ extmu}{ extmu}-calculus through a practical compiler implementation for programmers.

Findings

Successfully compiled a surface language into { extlambda}{ extmu}{ extmu}-calculus

Demonstrated the calculus's applicability as a compiler intermediate language

Made the sequent calculus more accessible to programming-language enthusiasts

Abstract

The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The {\lambda}{\mu}{\mu}-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 {\lambda}{\mu}{\mu}-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 {\lambda}{\mu}{\mu}-calculus as a compiler intermediate language.