Program logics:

reasoning principles for high-assurance software

Xavier Leroy

Collège de France, chair of software sciences, 2020-2021

This is an English translation of Xavier Leroy's 2020-2021 lectures at Collège de France, "Logiques de programmes : quand la machine raisonne sur ses logiciels".


Just like a mathematical logic enables us to prove properties of mathematical objects, a program logic enables us to prove properties of a computer program and of all its possible executions.

Program logics emerged in the 1960s with the seminal work of Floyd and of Hoare. Since the 2000s, program logics have tremendously progressed, with conceptual advances such as separation logics and impressive applications to the deductive verification of critical software. The course retraces these evolutions of program logics and, along with the companion seminar, presents a number of recent results in this area.


Companion Coq development

Parts of the lectures were mechanized using the Coq proof assistant. The commented Coq sources are available from the cdf-program-logics Github project.

Seminar talks

Some talks were given in English, others in French. Video recordings and slides can be found on the main course pages.