This is an English translation of Xavier Leroy's 2018-2019 lectures at Collège de France, "Programmer = démontrer? La correspondance de Curry-Howard aujourd'hui".

Computer science and mathematical logic are historically connected: Alan Turing, John von Neumann, Alonzo Church and many other computing pioneers were logicians, by trade or by training. My course for 2018-2019 studies another connection, this time of a mathematical nature, between programming languages and mathematical logics. In this approach, proving a theorem is equivalent to writing a program; stating a theorem is equivalent to partially specify a program by giving its expected type.

This correspondence between proving and programming was first observed on a simple case by two logicians: Haskell Curry in 1958, then William Howard in 1969. The result looked so insignificant that Howard never submitted it to a journal, privately circulating photocopies of his manuscript instead. Rarely have photocopies had such an impact: the Curry-Howard correspondence started to resonate with the renewal of logics and the boom of computer science of the 1970s, then established itself in the 1980s as a deep structural connection between languages and logics, between programming and proving.

Today, it is commonplace to study the logical meaning of a programming language feature, or the computational content of a mathematical theorem — that is, which algorithms hide inside its proofs. More importantly, the Curry-Howard correspondence gave birth to computing tools such as Coq and Agda, which are simultaneously programming langages and mathematical logics, and can be used for writing and verifying software as well as for stating and helping to prove mathematical results.

The course discusses this ferment of ideas, at the border between logic and computer science. It emphasizes recent results and open problems in this area. The companion seminar (in French) offered 7 experts an opportunity to present advanced results and complementary viewpoints.

**Introduction and course outline**[slides]- Lecture 1:
**The paths to discovery: the Curry-Howard correspondence, 1930–1970**[slides] - Lecture 2:
**Polymorphism all the way up! From System F to the Calculus of Constructions**[slides] - Lecture 3:
**Weapons of mass construction: inductive types, inductive predicates**[slides] - Lecture 4:
**You’ve got to decide one way or the other! Classical logic, continuations, and control operators**[slides] - Lecture 5:
**Can we change the world? Imperative programming, monadic effects, algebraic effects**[slides] - Lecture 6:
**Theorems for free: parametricity and logical relations**[slides] - Lecture 7:
**Forcing: just another program transformation?**[slides] - Lecture 8:
**Step carefully: step-indexing techniques**[slides] - Lecture 9:
**Sisyphus happy: infinite data types, proofs by coinduction, and reactive programming**[slides] - Lecture 10 :
**What is equality? From Leibniz to homotopy type theory**[slides] **Conclusions and discussion**[slides]

The talks were given in French. Video recordings and slides can be found on the main course pages.

- Pierre-Évariste Dagand:
*Les types dépendants: tout un programme!* - Assia Mahboubi:
*Mathématiques assistées par ordinateur* - Matthieu Sozeau:
*Programmer avec Coq: récursion et filtrage dépendant* - Guillaume Munch-Maccagnoni:
*Peut-on dupliquer un objet? Linéarité et contrôle des ressources* - Alexandre Miquel:
*Forcing et réalisabilité: vers l'unification* - Christine Tasson:
*Sémantique des programmes fonctionnels probabilistes, à la lumière de la logique linéaire* - Thierry Coquand:
*Du calcul des constructions à la théorie des types univalente*

Xavier.Leroy@college-de-france.fr