Gentzen-Mints-Zucker duality

TL;DR

This paper revisits Howard's work to interpret the Curry-Howard correspondence as a duality between local sequent calculus proofs and global lambda calculus or natural deduction, clarifying the logical and computational relationship.

Contribution

It presents a new perspective by framing the Curry-Howard correspondence as an isomorphism between proof categories, emphasizing the duality between local and global views.

Findings

Reinterprets Curry-Howard as a duality between proof categories

Highlights the distinction between local sequent calculus and global lambda calculus

Provides a categorical framework for understanding proof-program relationships

Abstract

The Curry-Howard correspondence is often described as relating proofs (in intutionistic natural deduction) to programs (terms in simply-typed lambda calculus). However this narrative is hardly a perfect fit, due to the computational content of cut-elimination and the logical origins of lambda calculus. We revisit Howard's work and interpret it as an isomorphism between a category of proofs in intuitionistic sequent calculus and a category of terms in simply-typed lambda calculus. In our telling of the story the fundamental duality is not between proofs and programs but between local (sequent calculus) and global (lambda calculus or natural deduction) points of view on a common logico-computational mathematical structure.