Changed on 08/04/2021
Sylvie Boldo, directrice de recherche au centre Inria Saclay - Île-de-France, animera un séminaire au Collège de France le jeudi 19 décembre dans le cadre des cours de Xavier Leroy.
  • Cours de Xavier Leroy 2019-2020 : "Sémantiques mécanisées : quand la machine raisonne sur ses langages"
  • Séminaire de Sylvie Boldo - Jeudi 19 décembre 2019 de 11h15 à 12h15 : "L’arithmétique des ordinateurs et sa formalisation"
Sylvie Boldo
© Inria / Photo G. Scagnelli

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.

Résumé du séminaire de Sylvie Boldo

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.

Biographie de Xavier Leroy

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.

Prix et distinctions

  •     Prix Michel Monpetit de l’Académie des sciences, 2007
  •     Prix Milner de la Royal Society , 2016
  •     Prix Van Wijngaarden du CWI (Centrum Wiskunde & Informatica) à Amsterdam, 2016
  •     Grand prix Inria-Académie des sciences, 2018
  •     Fellow de l'ACM (Association for Computing Machinery )