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: many computing pioneers, including Alan Turing, John von Neumann, and Alonzo Church, were logicians, by trade or by training. My 2018-2019 course studies another connection between programming languages and mathematical logics, this time of a mathematical nature. In this approach, proving a theorem is equivalent to writing a program, and stating a theorem is equivalent to partially specify a program by giving its expected type.
This correspondence between proving and programming was first observed in a simple case by two logicians: Haskell Curry in 1958 and William Howard in 1969. The result seemed so insignificant that Howard never submitted it to a journal and instead circulated photocopies of his manuscript privately. 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 in the 1970s, then established itself in the 1980s as a deep structural connection between languages and logics, and 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, the algorithms hidden inside its proofs. More importantly, the Curry-Howard correspondence has given rise 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 intersection of logic and computer science. It emphasizes recent results and open problems in this area. The companion seminar (in French) gave seven experts the opportunity to present advanced results and complementary viewpoints.
The talks were given in French. Video recordings and slides can be found on the main course pages.
Xavier.Leroy@college-de-france.fr