## Formal proof and Floating-Point Arithmetic

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/)