Xavier Leroy 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.
Xavier Leroy a été admis comme élève à l'École normale supérieure 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 , 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.
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. En 2018, il reçoit le Grand prix Inria-Académie des sciences et est nommé professeur au Collège de France sur la chaire de Sciences du logiciel.
Wikipedia
“A few programming is taking you away from mathematics; a lot will get you back in.”
Sources
Source: Xavier Leroy (2007) Conclusion of his seminar at Collège de France, 2009-03-13 http://www.college-de-france.fr/default/EN/all/inn_tec2007/seminaire_n3_xavier_leroy.htm,
Sources
Source: Xavier Leroy (2007-11-28), Post to the Caml mailing list, 2007-11-30 http://caml.inria.fr/pub/ml-archives/caml-list/2007/11/d7e444376489e889d3004f6c7d412713.en.html,
“If Bordeaux red wines were carbonated, McDonald's would be a lot more interested in selling them.”
Sources
Source: Xavier Leroy (2002-06-20), Post to the Caml mailing list, 2010-08-06 http://caml.inria.fr/pub/ml-archives/caml-list/2002/06/4d57fe13abe8b7823d9c5ca9379d37ce.en.html,
Sources
Source: Xavier Leroy (2005-07-23), Post to the Caml mailing list, 2008-02-20 http://caml.inria.fr/pub/ml-archives/caml-list/2005/07/0d3297c63e4b92fd956ea53d7b9ff255.en.html,
“Repeat after me: "Obj. magic is not part of the OCaml language."”
Sources
Source: Xavier Leroy (2009-10-28), Post to the Caml mailing list, 2009-10-28 http://article.gmane.org/gmane.comp.lang.caml.general/47389,
