INFO4213 : Preuves et programmes

These lectures introduce the Curry-Howard correspondence between proofs and programs, illustrating some of its key benefits. 
We present the natural deduction system for both intuitionistic and classical logic, discussing the properties and limitations of these systems. 
Furthermore, we establish a correspondence with the simply typed Lambda-Calculus and some of its extensions, such as the Lambda Mu-Calculus for classical natural deduction and System F for second-order propositional logic.

We will also prove some theorems that highlight the elegance of this correspondence, including the normalization and the parametricity theorems for System F.