Proofs and Programs
Contents of the course.
“Reasoning and programming are the two sides of the same coin”.
The core of this relation relies on the discovery of a very deep correspondence between Gentzen presentation for proofs of elementary statements from propositional calculus and typing Church’s λ-terms, named Curry-Howard correspondence (1980). Since then, the correspondence has been widely extended, which led toward powerful proof assistants and finer understanding of mathematical proofs; and correctness of programs as well.
Yet, until recently, equality was not properly understood, leaving on one side major mathematical techniques (congruences, quotients, …). In 2006 [Vladimir Voevodsky](Vladimir Voevodsky) envisioned a connection between equality proofs and homotopy. Since then, the relation between proofs and programs has regained a huge amount of attention. Recently (2015), a first contribution to providing a computational interpretation to the extended Type Theory HoTT has been proposed. We get closer to be able to do maths by programming!
- Lectures on C.-H. isomorphim, by M. H. Sørensen and P. Urzyczyn.
- Homotopy Type Theory, collaborative book (http://homotopytypetheory.org/)
- Logic (mainly Proof Theory, as opposed to Model Theory)
- Basics in Lambda-calculus
Webpage of the course: https://perso.ens-lyon.fr/philippe.audebaud/PnP/