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!

References.

  • Lectures on C.-H. isomorphim, by M. H. Sørensen and P. Urzyczyn.
  • Homotopy Type Theory, collaborative book (http://homotopytypetheory.org/)

Prerequisites.

  • 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/