11, place Marcelin-Berthelot
,
75005 Paris
Rendez-vous dans l'Amphithéâtre Guillaume Budé - Marcelin Berthelot
Les cours et séminaires au Collège de France sont gratuits, en accès libre, sans inscription préalable.
Nous confions à nos ordinateurs de nombreux calculs (météo, simulations aéronautiques, jeux vidéo, feuilles Excel ...) et nous considérons naturellement que l'ordinateur fournira une réponse juste.
Malheureusement, la machine a ses limites que l'esprit humain n'a pas. Elle utilise une arithmétique dite flottante qui a ses contraintes. D'une part chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. D'autre part, les valeurs que l'ordinateur appréhende ont des limites vers l'infiniment petit et l'infiniment grand. Hors de ces bornes, l'ordinateur produit des valeurs spéciales souvent inattendues. Pour plus de garanties, une formalisation de l'arithmétique flottante en Coq existe, permettant un haut niveau de confiance sur les résultats.
Xavier Leroy a étudié les mathématiques puis l'informatique à l'École normale supérieure et à l'université Paris-Diderot. Après un doctorat en informatique fondamentale en 1992 et un postdoctorat à l'université Stanford, il devient chargé de recherche à Inria en 1994, puis directeur de recherche en 2000. Il y dirige aujourd’hui l'équipe de recherche GALLIUM. De 1999 à 2004, il participe à la startup Trusted Logic . Il est nommé professeur au Collège de France en mai 2018 et devient le titulaire de la chaire Sciences du logiciel.
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 et du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.