Collège De France (général)

Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Leçon inaugurale : Le logiciel, entre l'esprit et la matière. Les travaux de recherche de Xavier LEROY portent d’une part sur les nouveaux langages et outils de programmation, et d’autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l’architecte et l’un des principaux développeurs du langage de programmation fonctionnelle OCaml ainsi que du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche. Langages fonctionnels, systèmes de types et mise en pratique : les langages Caml Light et OCaml Xavier LEROY a été formé aux mathématiques et à l’informatique à l’École normale supérieure, puis à l’INRIA où il a effectué sa thèse. Programmeur prodige, il s’est illustré par une série de travaux de premier plan sur les systèmes de types et les systèmes de modules pour les langages fonctionnels, qui ont abouti au développement de Caml Light, devenu aujou