Lecture 16: Curry-Howard Isomporphism

Guest lecturer: Valery Trifonov.

In this lecture we present the Curry-Howard algorithm as a relation between the simply typed lambda calculus and the natural deduction calculus. First, we show that propositions are represented as types, proofs as terms, local reductions as beta, cut elimination as normalization etc. Second, we define a term language for natural deduction: lambda calculus plus first-class continuations (for negation), i.e. something like lambda-mu. Third, we define a term language for Gentzen's sequent calculus (with cut), i.e. an A-normal form calculus (plus extensions for negation). And forth, we give a translation from the former to the latter and its correspondence to Thm 3.10 (completeness of sequent calculus w/ cut) of Pfenning's notes on sequent calculus.

Suggested Reading Materials:

Frank Pfenning. Sequent Calculus