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

Basic number systems
Basic arithmetic algorithms
Floating-point arithmetic: main properties

2. Floating-point and alternative systems

The IEEE 754 standard and its 2019 revision.
New formats and instructions (NVIDIA's GPUs, Google's TPUs, ...)
Alternatives to floating-point (fixed-point, LNS block floating-point, tapering, posits, ...)

3. Rigorous analysis of algorithms in floating-point

Standard models and worst-case error bounds
Enhanced analysis via low-level properties of IEEE 754
Probabilistic models and statistical error analysis

4. Various recent applications

Elementary functions and libm implementation
Mixed precision for faster yet accurate linear algebra
Low precision for machine learning

5. advanced FP arithmetic

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

6. Beyond basic arithmetic

    double-words
    building blocks of complex arithmetic

Bibliography:

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

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