Curry-Howard correspondence for Ni and Church-Rosser theorem
We would like to illuminate the Curry-Howard correspondence for the intuitionistic natural deduction systems and the simply typed lambda calculus. For ease of exposition we would like to focus on natural deduction systems for propositional logic using implication as the only connective. This corresponds to ->Npi in Troelstra-Schwichtenberg terminology.
The two main goals of the presentation will be to develop and explain the proofs-as-programs interpretation and to further show the correspondence between the reduction of Lambda-terms and the normalisation of proofs in natural deduction systems in light of the Church-Rosser and the Normalization theorems.
- Lectures on the Curry-Howard Isomorphism (1998) by Morten Heine B. Sørensen, Pawel Urzyczyn
- Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor
- Basic Proof Theory by A. S. Troelstra, H. Schwichtenberg