Xavier Leroy a étudié les mathématiques puis l'informatique à l'École normale supérieure et à l'université Paris-Diderot. Après un doctorat en informatique fondamentale en 1992 et un postdoctorat à l'université Stanford, il devient chargé de recherche à l'Inria en 1994, puis directeur de recherche en 2000. De 2006 à 2019, il y dirige l'équipe de recherche Gallium. De 1999 à 2004, il participe à la start-up Trusted Logic. Il est nommé professeur du Collège de France en mai 2018 et devient le titulaire de la chaire Sciences du logiciel.
Les travaux de recherche de Xavier Leroy visent à améliorer, à l’aide d’approches rigoureuses et mathématiquement fondées, la sûreté, la sécurité et la facilité de développement de logiciels critiques. Il étudie, d'une part, les nouveaux langages et outils de programmation s'appuyant sur le paradigme fonctionnel, et, de l'autre, la vérification formelle de logiciels critiques par vérification déductive et par analyse statique. Il est l'architecte et l’un des principaux développeurs du langage de programmation fonctionnelle OCaml et du compilateur formellement vérifié CompCert, deux grands logiciels issus de la recherche.
Prix et distinctions
- 2007 : Prix Michel-Monpetit de l’Académie des sciences
- Depuis 2015 : Fellow de l'ACM (Association for Computing Machinery)
- 2016 : Prix Milner de la Royal Society
- 2016 : Prix Van Wijngaarden du CWI (Centrum Wiskunde & Informatica) à Amsterdam
- 2018 : Grand prix Inria-Académie des sciences
- 2022 : ACM Software System Award
