Floating-point arithmetic and beyond

Lecturers: Sylvie Boldo Claude-Pierre Jeannerod, Guillaume Melquiond and Jean-Michel Muller.

Summary: Computer arithmetic is currently undergoing a major
evolution, with traditional IEEE floating-point being complemented
with new formats and instructions, but also with alternative number
systems. This course will present these recent developments (mostly
driven by new needs in HPC and AI), with an emphasis on both
application examples and state-of-the-art techniques for rigorously analyzing the behavior of numerical algorithms.

Tentative outline:

1. Basic concepts of Computer arithmetic

2. Floating-point and alternative systems

3. Rigorous analysis of algorithms in floating-point

4. Various recent applications

5. advanced FP arithmetic

    FP arithmetic and compilers
    tools for computer-assisted analysis of numerical programs

6. Beyond basic arithmetic

    building blocks of complex arithmetic


Handbook of Floating-Point Arithmetic, 2nd ed., 2018.

Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System