Xavier Leroy's photo

Hello and welcome to my corner of the Web. I'm a senior computer scientist interested in all scientific aspects of computer programming. I'm a professor at Collège de France, where I hold the chair of software sciences. I'm also a member of the Cambium research team of Inria, a French public research institute in computer science and applied mathematics.


[07/2021] Lecture material: slides in English are now available for my Collège de France lectures on Program logics.

[11/2020] Publication: Verified Code Generation for the Polyhedral Model, by Nathanaël Courant and I, to be presented at POPL 2021, with accompanying Coq development.

[10/2020] Lecture material: slides in English are now available for my Collège de France lectures on The Curry-howard correspondence today (2018-2019) and on Mechanized semantics (2019-2020). See also the companion Coq development.

[12/2019] Publication: the text of my inaugural lecture at Collège de France, Software, between mind and matter, is now available freely: in the original French at OpenEdition Books (HTML) and at HAL (PDF); and in English through a preliminary translation (PDF and e-book).

[04/2019] Publication (in French): the text of my inaugural lecture at Collège de France, Le logiciel, entre l'esprit et la matière, is now available as a book and an e-book. The video of the lecture is still available, in the original French, but also with an English voice-over translation.

[11/2018] Appointment: I am proud to be appointed professor at Collège de France on the chair of software sciences. It's a great honor but also a great responsibility! (This is the second permanent chair in computer science at Collège de France, after Gérard Berry's chair.)

[07/2018] Award: I am honored to receive the Grand prix Inria - Académie des sciences 2018.

[01/2018] Publication: CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler, by Daniel Kästner et al, presented at ERTS 2018. This paper describes the first use of CompCert in production for a safety-critical application in the nuclear industry, including IEC 60880 certification.

[12/2017] I was interviewed by Jean Yang as part of a "People of Programming Languages" series.

[06/2017] Publication: A Formally Verified Compiler for Lustre, by Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, myself, Marc Pouzet and Lionel Rieg, PLDI 2017.

[02/2017] Software and Coq development: version 3.0 of Compcert is released. This is the first CompCert version that fully supports 64-bit target processors; more precisely, pointers and memory addresses are no longer assumed to be 32-bit wide and can be 64-bit wide as well depending on the target. Definitely 3.0 material!

[11/2016] Public lecture: video of my Milner award lecture at the Royal Society.

[11/2016] Award: I am deeply honored to receive one of the two 2016 van Wijngaarden awards from CWI.

[01/2016] Award: my POPL 2006 paper, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, received the ACM SIGPLAN Most Influential POPL Paper Award.

Older news...