Approximation Theory and Proof Assistants: Certified Computations

Master d'informatique fondamentale of École Normale Supérieure de Lyon, Fall-Winter 2018.

As of today, when it comes to perform numerical computations such as integrals, global optimization, etc. most scientist or engineers use well-known software like MATLAB or Maple, and numerical analysis-based routines that they offer. Though effective and correct most of the time, these results are returned with no guaranty at all on their quality (such as a certified error, say). This can be a real issue in various contexts where reliability and accuracy of computations are at stake. Examples include not only computational methods for hard mathematical problems appearing in nonlinear dynamics, but also practical critical systems such as control units of aircrafts or particle accelerators for instance.

In this course, we will present some aspects of the theory of polynomial approximation, we will introduce you with the Coq proof assistant and we will combine both subjects to address some examples of certified computations.

Lecture notes and slides of the course Coq practical sessions Organisation Evaluation References


Lecture notes and slides of the course

You can have a look at a draft version of the lecture notes.

Coq practical sessions

Please see Damien's dedicated page.





Lecture notes


More advanced level:

PhD theses