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 |

- Next course: 11/2, 8:00 am, online (click there or see the pad for the connection informations).
- Tentative schedule: lectures on the 9/9 (NB), 9/14 (DP), 9/16 (NB), 9/21 (DP), 9/23 (NB), 9/28 (DP), 9/30 (NB), 10/5 (DP), 10/7 (NB), 10/12 (DP), 10/14 (DP), 10/19 (DP), 10/21 (MJ), 10/22 (DP), 11/2 (DP). Exam on the 4th of November, from 10:15 am to 12:15 am, in rooms B1 and B2 (4th floor of the GN1 building).

- Slides of class n.1, 9/9/2020, corresponds to pages 5-9 of the lecture notes.
- Slides of class n.2, 9/16/2020, corresponds to pages 9-14 of the lecture notes.
- Slides of class n.3, 9/23/2020, corresponds to pages 14-21 of the lecture notes.
- Slides of class n.4, 9/30/2020, corresponds to pages 21-32 of the lecture notes.
- Slides of class n.5, 10/7/2020, corresponds to pages 33-39 and 43-49 of the lecture notes.

- Hours : Mondays from 8:00 am to 10:00 am and Wednesdays from 10:15 am to 12:15 am. Damien Pous's courses are delivered online (see the pad for the connection informations) and Nicolas Brisebarre's courses are delivered in room B1 (4th floor of the main building of ENS Lyon, Monod part).
- Teachers: Nicolas Brisebarre and Damien Pous.
- The lectures will be delivered in French or English on request.

- Evaluation: Two small Coq projects and a final pen and paper exam.

- J. B. van den Berg and J.-P. Lessard. Rigorous Numerics in Dynamics. Notices of the AMS, 1057-1061, Oct. 2015.

- Algorithmes efficaces en calcul formel (in French), lecture notes by A. Bostan, F. Chyzak, G.Lecerf and B. Salvy. Parisian Master of Research in Computer Science.

- Y. Bertot and P. Castéran. The Coq'Art.
- A. Chlipala. Certified Programming with Dependent Types, The MIT Press, 2013.
- J.-P. Demailly. Analyse numérique et équations différentielles. EDP Sciences.
- J. von zur Gathen and J. Gerhard. Modern Computer Algebra, Cambridge University Press.
- J. C. Mason and D. C. Handscomb. Chebyshev Polynomials. Chapman & Hall/CRC.
- B. Pierce et al. Software Foundations.
- M. Schatzman. Analyse numérique, une approche mathématique. Dunod. And in English: Numerical Analysis: A Mathematical Introduction. Oxford University Press.
- L. N. Trefethen. Approximation Theory and Approximation Practice.
- W. Tucker. Validated Numerics, a short introduction to rigorous computations. Princeton University Press.

- C. M. Bender and S. A. Orszag. Advanced mathematical methods for scientists and engineers, McGraw-Hill Book Co..
- D. Bini and V. Y. Pan. Polynomial and Matrix Computations, Volume 1: Fundamental Algorithms, Birkhäuser.
- J. P. Boyd. Chebyshev and Fourier Spectral Methods. Dover.
- E. W. Cheney. Introduction to Approximation Theory. AMS Chelsea Pub.
- A. Gil, J. Segura and N. M. Temme, Numerical methods for special functions, Society for Industrial and Applied Mathematics (SIAM).
- E. W. Kaucher et W. L. Miranker. Self-validating numerics for function space problems. Academic Press, 1984.
- R. Moore and M. J. Cloud. Computational functional analysis. Horwood Pub.
- M. Powell. Approximation theory and methods. Cambridge University Press.
- L. B. Rall. Computational Solution of Nonlinear Operator Equations. John Wiley & Sons Ltd.

- A. Benoit, Algorithmique semi-numérique rapide des séries de Tchebychev. Thèse de doctorat, École Polytechnique, juillet 2012
- F. Bréhard, Certified numerics in function spaces : polynomial approximations meet computer algebra and formal proof. Thèse de doctorat, École Normale Supérieure de Lyon, juillet 2019
- S. Chevillard, Évaluation efficace de fonctions numériques - Outils et exemples. Thèse de doctorat, École Normale Supérieure de Lyon, septembre 2011
- P. Di Lizia, Robust Space Trajectory and Space System Design using Differential Algebra, Politecnico di Milano, 2008
- M. Joldeş, Rigorous Polynomial Approximations and Applications. Thèse de doctorat, École Normale Supérieure de Lyon, septembre 2011
- É. Martin-Dorel, Contributions to the Formal Verification of Arithmetic Algorithms. Thèse de doctorat, École Normale Supérieure de Lyon, septembre 2012
- M. Mezzarobba, Autour de l'évaluation numérique des fonctions D-finies, Thèse de doctorat, École Polytechnique, octobre 2011

- Chebfun, numerical computing with functions
- The Coq proof assistant
- Flocq (Floats for Coq)
- Maple
- Mathemagix
- Pari/GP
- Sage, a free open-source mathematics software. A nice presentation (in French) is available here
- Scilab
- Sollya