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.
The talks were given in French. Video recordings and slides can be found on the main course pages.
Xavier.Leroy@college-de-france.fr