Résumé
Le deuxième séminaire était consacré à la sémantique formelle des calculs numériques. La conférencière a rappelé les principes de la représentation approchée des nombres réels par des nombres en virgule flottante à précision limitée, ainsi que les spectaculaires « bugs » qui se produisent lorsque l’arithmétique à virgule flottante est mal utilisée ou mal implémentée. Elle a ensuite décrit le projet Flocq de mécanisation en Coq de l’arithmétique à virgule flottante, et ses utilisations pour vérifier formellement des routines de calcul numérique aussi bien que des algorithmes de génération de code et d’optimisation dans les compilateurs.
