Logo

Programming = proving?

The Curry-Howard correspondence today

Xavier Leroy

Collège de France, chair of software sciences, 2018-2019

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".

Abstract

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. The 2018-2019 course in the software sicences chair 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 logic and the explosion 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 rise to computing tools such as Coq and Agda which are simultaneously programming langages and mathematical logics, and can be used equally well for writing and verifying software and 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.

Lectures

Seminar talks

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


Xavier.Leroy@college-de-france.fr