Gentzen–Mints–Zucker duality

Abstract The Curry–Howard correspondence is often described as relating proofs (in intuitionistic 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 the lambda calculus. We revisit Howard’s work and interpret it as an isomorphism between a category of formulas and proofs in intuitionistic sequent calculus and a category of types and terms in simply-typed lambda calculus. In our telling of the story, the fundamental duality is not between proofs and programs but between emphlocal (sequent calculus) and global (lambda calculus or natural deduction) points of view on a common logico-computational mathematical structure.