Sequent Calculus as a Compiler Intermediate Language

2016 by Paul Downen, Luke Maurer, Zena M. Ariola, Simon Peyton Jones

The typed λ-calculus arises canonically as the term language for a logic called natural deduction, using the Curry-Howard isomorphism: the pervasive connection between logic and programming languages asserting that propositions are types and proofs are programs. Indeed, for many people, the λ-calculus is the living embodiment of Curry-Howard.

But natural deduction is not the only logic! Conspicuously, natural deduction has a twin, born in the very same paper, called the sequent calculus. Thanks to the Curry-Howard isomorphism, terms of the sequent calculus can also be seen as a programming language with an emphasis on control flow.

## Recent comments

1 day 21 hours ago

2 days 7 min ago

2 days 19 hours ago

3 days 2 hours ago

3 days 6 hours ago

3 days 6 hours ago

3 days 8 hours ago

4 days 3 min ago

4 days 4 hours ago

1 week 11 hours ago