This course introduces the Curry-Howard correspondence between formal proofs and programs, which is at the core of modern proof assistants such as Rocq. It provides a foundational perspective on the relationship between proof-theory and computation, showing how proofs can be understood as computational objects and how derivation rules can be interpreted as program construction.

We start with the correspondence between the simply typed λ-calculus and intuitionistic propositional natural deduction, and extend it to broader frameworks, including continuations and classical logic, parametric polymorphism and second-order quantification.
We study proofs of major results, such as normalization of typed calculi, coherence theorems for natural deduction, conservativity and parametricity of System F.

Lab sessions may optionally involve formalizing parts of the lectures using Rocq.