Xavier Leroy
Pour les articles homonymes, voir Leroy.
Pour le danseur et chorégraphe, voir Xavier Le Roy
Xavier Leroy
| Naissance | |
|---|---|
| Nationalité | française  |
| Formation | École normale supérieure Université Paris-Diderot |
| Activités | Informaticien, programmeur, ingénieur, professeur d'université |
| A travaillé pour | Institut national de recherche en informatique et en automatique (France) (d) ( - Inria Collège de France Université de Paris |
|---|---|
| Membre de | |
| Directeur de thèse | |
| Site web | xavierleroy.org |
| Distinctions | Liste détaillée Prix Michel-Monpetit () ACM Fellow () Prix Milner () Prix Van Wijngaarden () Grand prix Inria - Académie des sciences () |
modifier - modifier le code - modifier Wikidata
Xavier Leroy (né le ) est un informaticien français, professeur au Collège de France et précédemment directeur de recherche à l'INRIA. Il est connu pour être le principal concepteur et développeur du langage Objective Caml ainsi que pour ses travaux sur le compilateur formellement vérifié CompCert.
Cursus et travaux
Xavier Leroy a été admis comme élève à l'École normale supérieure (Paris) en 1987, et y a étudié les mathématiques et l'informatique. De 1989 à 1992 il a fait sa thèse de doctorat sous la direction de Gérard Huet.
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.
Il est également l'auteur de LinuxThreads (en), qui était, avant la sortie de la version 2.6 du noyau Linux, la bibliothèque de threads la plus utilisée dans le système Linux.
Il est élu membre de l'Académie des sciences en 2022[1].
Honneurs
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].
Notes et références
- ↑ Académie des sciences, « 18 nouveaux membres élus à l’Académie des sciences » [PDF] (communiqué de presse), (consulté le )
- ↑ « CWI soiree & Van Wijngaarden Award Ceremony » [archive du ], Centrum Wiskunde & Informatica, (consulté le )
- ↑ « Lauréats des prix 2018 », sur Académie des sciences, (consulté le )
- ↑ « Leçon inaugurale de Xavier Leroy », sur Collège de France, (consulté le )
- ↑ https://www.sigplan.org/Awards/Software/
Liens externes
- Page personnelle de Xavier Leroy
- Ressources relatives à la recherche
: - Academia (profils)
- Collège de France
- Digital Bibliography & Library Project
- Google Scholar
- Mathematics Genealogy Project
- ORCID
- ResearchGate
- Notices d'autorité :
- VIAF
- ISNI
- BnF (données)
- IdRef
- LCCN
- Pays-Bas
- Israël
- WorldCat
Portail de l'informatique théorique 
Portail de la programmation informatique
