Abstract
The second seminar was devoted to the formal semantics of numerical computations. The speaker recalled the principles of the approximate representation of real numbers by floating-point numbers with limited precision, as well as the spectacular " bugs " that occur when floating-point arithmetic is misused or poorly implemented. She then described the Flocq project to mechanize floating-point arithmetic in Coq, and its uses for formally verifying numerical computation routines as well as code generation and optimization algorithms in compilers.
