Xavier Leroy studied mathematics and computer science at the École normale supérieure and Université Paris-Diderot. After a PhD in fundamental computer science in 1992 and a post-doctorate at Stanford University, he became a research fellow at Inria in 1994, then research director in 2000. From 2006 to 2019, he headed the Gallium research team. From 1999 to 2004, he was involved in the start-up Trusted Logic. He was appointed Professor at the Collège de France in May 2018, and holds the Software Sciencechair.
Xavier Leroy's research aims to use rigorous, mathematically-based approaches to improve the safety, security and ease of development of mission-critical software. On the one hand, he studies new programming languages and tools based on the functional paradigm, and on the other, formal verification of critical software by deductive verification and static analysis. He is the architect and one of the main developers of the OCamlfunctional programming language and the CompCert formally verified compiler , two major software products resulting from his research.
