WG211/M7Stump
Purifying Natural Deduction Using Sequent Calculus
Aaron Stump
The Curry-Howard isomorphism has proved a very fruitful connection between programming languages and logic for the past 30 years or so. Proofs in intuitionistic natural deduction are identified with terms in typed lambda calculus, and various notions of reduction and equivalence of terms can then be exchanged between the logical and computational views. The case of disjunction (sum types) and existentials has not worked out so cleanly, however, requiring so-called commuting conversions. In this talk, I show how to remove the difficulties for disjunctions and existentials, by introducing new lambda calculus terms. These terms arise from a new and more direct term assignment to proofs in sequent calculus. The result is a type system for which we can easily adapt Girard's reducibility candidates to show strong normalization, and for which notions of extensionality for sum types and existentials become natural to state and accomodate in our notions of term reduction and equivalence. Both these results have been problematic with the traditional terms for disjunctions and existentials.
- stump-wg09.pdf : Slides
