What Functional Programmers Can Learn from Sequent Calculus

This article highlights five key insights from the 𝜆𝜇𝜇˜-calculus, particularly the treatment of evaluation contexts as first-class and the restored symmetry between data and codata in sequent calculus. These features simplify reasoning and implementation in functional languages by clarifying evaluation order and reducing conceptual asymmetries in type systems.

Table of Links

A. The Relationship to the Sequent Calculus

B. Typing Rules for Fun

C. Operational Semantics of label/goto

References

5 Insights

In the previous section, we have explained what the 𝜆𝜇𝜇˜-calculus is, and how it works. Now that we know the what and how we can explain why this calculus is so interesting. This section is therefore a small collection of independent insights. To be clear, these insights are obvious to those who are deeply familiar with the 𝜆𝜇𝜇˜-calculus, but we can still recall how surprising they were for us when ...