Accueil/ conferencier
Xavier Leroy

Cursus :

Ancien élève de l'Ecole normale supérieure, Xavier Leroy est un informaticien français, directeur de recherche à l'INRIA. Il est connu pour être le principal concepteur et développeur du langage Objective Caml.

Il 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 Montpetit. 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.

Affiliation : INRIA

Statut : Informaticien

Exposé(s) :
photoExpose
Comment faire confiance à un compilateur ?
Xavier Leroy

Conférence de Xavier Leroy dans le cadre du Séminaire général du département d’informatique

Le logiciel critique - celui dont dépendent des vies humaines - nécessite des techniques de développement et de validation très part...
Mots-clés : analyseur , Code , compilateur , Langage , logiciel , programmation , Séminaire général du département d'informatique