This workshop gathered specialists of computer arithmetic, formal proof systems, computer algebra, rigorous computing and optimal control theory. The aim was to exchange tools and ideas to develop computer-aided proofs of numerical values, with certified and reasonably tight error bounds, without sacrificing efficiency.

This workshop concluded a project funded by the French ANR. It was open to members of that project and to colleagues of various origins sharing our interest in these topics.

The workshop took place in ENS de Lyon, Campus Descartes, Room D2 034.

# Invited Speakers

- Bernhard Beckermann
- Khalil Ghorbal
- Javier Segura
- Vincenzo Innocente
- Juliette Leblond
- Lloyd N. Trefethen
- Warwick Tucker

# Registration

Registration is free, but necessary (we need it to plan badges, coffee breaks, lunches). Please use the registration form (before April 15.)# Program

### Wednesday, May 22

- 10:00
- Welcome
- 10:30
**Lloyd N. Trefethen***New Laplace and Helmholtz solvers*Slides- 11:30
**Florent Bréhard***A certificate-based approach to formally verified approximations*Slides- 12:00
- Lunch
- 14:30
**Javier Segura***Computation of classical orthogonal polynomials and their associated Gauss quadrature rules*Slides- 15:30
**Jean-Michel Muller***Error analysis of some operations involved in the Fast Fourier Transform*Slides- 16:00
**Guillaume Melquiond***Formal Verification of a State-of-the-Art Integer Square Root*Slides- 16:30
- Break
- 17:00
**Juliette Leblond***About some inverse magnetic moment estimation problems and computations of numerical magnetometers*Slides- 18:00
**Nicolas Brisebarre***Exponential sums and correctly-rounded functions*Slides

### Thursday, May 23

- 10:00
**Vincenzo Innocente***Small, Fast, Accurate: Arithmetic Challenges in Particle Physics*Slides (big file)- 11:00
**Sylvie Boldo***Formal verification about the floating-point average*Slides- 11:30
**Fredrik Johansson***Fungrim: the Mathematical Functions Grimoire*Slides- 12:00
- Lunch
- 14:30
**Khalil Ghorbal***Formal Verification and Generation of Semi-Algebraic Invariant Sets for Polynomial Autonomous ODEs.*Slides- 15:30
**Marc Mezzarobba***Recent improvements to the ore_algebra package*Slides- 16:00
**Laurent Théry***Computing Chebyshev models in Coq*Slides- 16:30
- Break
- 17:00
**Bernhard Beckermann***Solving singular integral equations with orthogonal rational functions*- 18:00
**Mioara Joldes***On moment problems with holonomic functions*