Due to its efficiency (very fast arithmetic operators, possibility of representing huge as well as tiny numbers), floating-point (FP) arithmetic is used everywhere in scientific computing. The large-scale calculations required to deal with problems of fluid mechanics, for instance, could not be done in a reasonable delay without floating-point arithmetic.
However, its intrinsically approximate aspect may lead to several problems (rounding errors may accumulate). Also, erroneous or naive programing may make the behavior of programs difficult to predict.
Also, most users are not aware of the fact that the behavior of the FP arithmetic operations is now fully specified (IEEE 754 standard), so that one may elaborate proofs and use the specifications. This is a very important issue when FP arithmetic is used in a context where a mistake could have serious consequences (air transport, control of hazardous physico / chemical processes, etc.).
The purpose of this course is to first introduce students to "subtle" properties of floating point arithmetic: with the requirements of the IEEE 754 standard, you can build and prove algorithms that allow to perform "exact" (or very accurate) calculations (examples are polynomial evaluation, matrix calculations, etc.) based on this "approximate" arithmetic. We then focus on the possibility of developing formal proofs of floating-point algorithms and programs, illustrating this point by the formalization, using the Coq proof assistant, of FP arithmetic.
The course will be given by Jean-Michel Muller (CNRS, Laboratoire LIP: http://perso.ens-lyon.fr/jean-michel.muller/), Damien Pous (CNRS, Laboratoire LIP: http://perso.ens-lyon.fr/damien.pous/index.html), and Laurent Théry (INRIA Sophia Antipolis: http://www-sop.inria.fr/marelle/Laurent.Thery/moi.html).
For their evaluation, the students will have to analyse a recent scientific paper.
It is *not* requested that the students have a preliminar knowledge of Coq: some sessions will be devoted to give them the necessary knowledge.
A few references:
- The recent "Handbook of Floating-Point Arithmetic"
(http://perso.ens-lyon.fr/jean-michel.muller/Handbook.html)
- Guillaume Melquiond's page (http://www.lri.fr/~melquion/)