Xavier Leroy

L'ACM salue les travaux de Xavier Leroy sur les langages de programmation et les compilateurs, leur fiabilité et leur sécurité. Sa plongée dans le monde des méthodes formelles l’oriente vers la vérification des logiciels critiques, dont le dysfonctionnement pourrait avoir un impact important sur la sécurité des personnes et des entreprises, comme ceux qui équipent certaines cartes à puce ou encore les métros sans conducteur. Xavier Leroy a travaillé sur la fiabilité et la qualité du logiciel grâce à une approche focalisée sur les langages de programmation. Travaux qui aboutissent notamment au langage OCaml désormais utilisé dans la recherche ainsi que par de nombreux industriels, dans la finance, la sécurité, ou encore le Web. Il cherche également à démontrer mathématiquement la fiabilité d’un logiciel, en particulier des compilateurs. Ces derniers sont chargés de traduire un code source dans un langage de programmation en un langage machine et sont essentiels à la sécurisation des logiciels critiques. En découle le compilateur CompCert. Actuellement professeur au Collège de France, Xavier Leroy y développe une approche des sciences du logiciel qui repose sur les fondements mathématiques et logiques de la programmation.