Xavier Leroy

Xavier Leroy, membre de l’Académie des sciences, professeur au Collège de France, titulaire de la chaire Sciences du logiciel.

Xavier Leroy est un informaticien qui étudie la science de la programmation des ordinateurs, de la conception des langages de programmation à la vérification des logiciels. Ses travaux de recherche visent à améliorer, à l’aide d’approches rigoureuses et mathématiquement fondées, la sûreté (strict respect du comportement spécifié), la sécurité (résistance aux attaques externes) et la facilité de développement de logiciels critiques, ceux dont dépendent des vies humaines ou des infrastructures essentielles. Il est l'architecte et l’un des principaux développeurs d'OCaml, un langage de programmation fonctionnelle parmi les plus utilisés dans l'industrie, la finance, le Web, mais aussi pour l'enseignement de l'informatique en France et à l’étranger.  Il est également le concepteur et le principal développeur du compilateur CompCert, le premier compilateur formellement vérifié pour le langage C. Les compilateurs, ces programmes chargés de traduire un code source écrit dans un langage de haut niveau en langage machine, sont des rouages essentiels de la chaîne de sécurisation des logiciels critiques.

--> Site Web