Xavier Leroy's mugshot

Hello and welcome to my corner of the Web. I'm a senior computer scientist interested in all scientific aspects of computer programming. I work at INRIA, a French public research institute in computer science and applied mathematics. I lead the Gallium research team, part of the Paris research center center of INRIA.


[05/2018] Appointment: I am proud to be appointed professor of Software sciences at Collège de France, starting this Fall. 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.)

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