Xavier Leroy est un expert réputé dans le domaine des langages fonctionnels, de leur typage et de leur compilation. Ces dernières années, il a également beaucoup travaillé sur les méthodes formelles, les preuves formelles et la compilation certifiée. Il est notamment à la base du projet CompCert qui a réalisé un compilateur pour le langage C entièrement certifié à l'aide de Coq.
L'équipe de développement d'OCaml recevant le SIGPLAN programming Languages Software Award en 2023 à la conférence POPL 2024
En 2007, Xavier Leroy est lauréat du Prix Monpetit. En 2011, il est lauréat du prix La Recherche en sciences de l'information, en tant que représentant du projet CompCert. En 2012, il reçoit le prix « Microsoft Research Verified Software Milestone Award Citation », là encore en tant qu'architecte de CompCert. En 2016, il est lauréat du prix Milner « en reconnaissance de ses réalisations exceptionnelles dans la programmation informatique », la même année il reçoit également le prix Van Wijngaarden[2]. En 2018, il reçoit le Grand prix Inria-Académie des sciences[3] et est nommé professeur au Collège de France sur la chaire de Sciences du logiciel[4]. En 2022, lui et six de ses collaborateurs de CompCert reçoivent le prix ACM Software System 2021. Lui et le reste de l'équipe de développement de CompCert reçoivent le SIGPLAN Programming Languages Software Awar en 2022; lui et le reste de l'équipe de développement d'OCaml reçoivent le même prix 2023[5].
