H. Barendregt and E. Barendsen, Autarkic computations in formal proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002.

A. Benoit, M. Jolde?, and M. Mezzarobba, Rigorous uniform approximation of D-finite functions using Chebyshev expansions, Math. Comp, vol.86, issue.305, pp.1303-1341, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01022420

V. Berinde, Iterative approximation of fixed points, Lecture Notes in Mathematics, vol.1912, 2007.

M. Berz and K. Makino, Verified integration of odes and flows using differential algebraic methods on high-order Taylor models, Reliable Computing, vol.4, issue.4, pp.361-369, 1998.

S. Boldo, F. Clément, F. Faissole, V. Martin, and M. Mayero, A Coq formal proof of the Lax-Milgram theorem, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01391578

S. Boldo and G. Melquiond, Verifying Floating-point Algorithms with the Coq System, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01632617

N. Bourbaki, . Topology, and . Springer, Original French edition published by MASSON, 1971.

F. Bréhard, N. Brisebarre, and M. Joldes, Validated and numerically efficient Chebyshev spectral methods for linear ordinary differential equations, ACM Transactions on Mathematical Software, 2018.

F. Bréhard, N. Brisebarre, M. Joldes, and W. Tucker, A New Lower Bound on the Hilbert Number for Quartic Systems, 2019.

N. Brisebarre and M. Jolde?, Chebyshev interpolation polynomial-based tools for rigorous computing, Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, pp.147-154, 2010.
URL : https://hal.archives-ouvertes.fr/ensl-00472509

F. Bréhard, A. Mahboubi, and D. Pous,

O. Caprotti and M. Oostdijk, Formal and efficient primality proofs by use of computer algebra oracles, J. Symb. Comput, vol.32, issue.1, pp.55-70, 2001.

C. Christopher, Estimating limit cycle bifurcations from centers, Differential equations with symbolic computation, pp.23-35, 2005.

A. Tobin, N. Driscoll, L. N. Hale, and . Trefethen, , 2014.

L. Fox and I. B. Parker, Chebyshev polynomials in numerical analysis, 1968.

B. Grégoire and A. Mahboubi, Proving equalities in a commutative ring done right in coq, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs, vol.3603, pp.98-113, 2005.

B. Grégoire and L. Théry, A purely functional library for modular arithmetic and its application to certifying large prime numbers, Automated Reasoning, Third International Joint Conference, vol.4130, pp.423-437, 2006.

C. Thomas, M. Hales, G. Adams, D. Bauer, J. Dang et al., , 2015.

J. Harrison and L. Théry, A skeptic's approach to combining HOL and maple, J. Autom. Reasoning, vol.21, issue.3, pp.279-294, 1998.

J. Hölzl, F. Immler, and B. Huffman, Type classes and filters for mathematical analysis in isabelle/hol, Interactive Theorem Proving, pp.279-294, 2013.

A. Hungria, J. Lessard, and J. D. James, Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach, Math. Comp, vol.85, issue.299, pp.1427-1459, 2016.

F. Immler, A verified ODE solver and the Lorenz attractor, Journal of automated reasoning, pp.1-39, 2018.

F. Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic, IEEE Transactions on Computers, vol.66, issue.8, pp.1281-1292, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01394258

T. Johnson, A quartic system with twenty-six limit cycles, Exp. Math, vol.20, issue.3, pp.323-328, 2011.

M. Jolde?, Rigorous Polynomial Approximations and Applications, 2011.

W. Edgar, W. L. Kaucher, and . Miranker, Self-validating numerics for function space problems: Computation with guarantees for differential and integral equations, vol.9, 1984.

R. Klatte, U. Kulisch, A. Wiethoff, and M. Rauch, C-XSC: A C++ class library for extended scientific computing, 2012.

J. , P. Lessard, and C. Reinhardt, Rigorous numerics for nonlinear differential equations using Chebyshev series, SIAM J. Numer. Anal, vol.52, issue.1, pp.1-22, 2014.

A. Mahboubi, G. Melquiond, and T. Sibut-pinote, Formally verified approximations of definite integrals, Journal of Automated Reasoning, vol.62, issue.2, pp.281-300, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01289616

É. Martin, -. Dorel, and G. Melquiond, Proving tight bounds on univariate expressions with elementary functions in coq, Journal of Automated Reasoning, vol.57, issue.3, pp.187-217, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01086460

G. Melquiond, Proving bounds on real-valued functions with computations, International Joint Conference on Automated Reasoning, pp.2-17, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00180138

R. E. Moore, Interval Analysis, 1966.

N. Revol and F. Rouillier, Motivations for an arbitrary precision interval arithmetic and the mpfi library, Reliable computing, vol.11, issue.4, pp.275-290, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00100985

M. Siegfried and . Rump, Intlab-interval laboratory, Developments in reliable computing, pp.77-104, 1999.

L. Nicholas-trefethen, Approximation Theory and Approximation Practice. SIAM, 2013.

W. Tucker, A rigorous ODE solver and Smale's 14th problem, Found. Comput. Math, vol.2, issue.1, pp.53-117, 2002.

W. Tucker, Validated numerics: a short introduction to rigorous computations, 2011.

J. Bouwe-van-den, J. Berg, and . Lessard, Chaotic braided solutions via rigorous numerics: Chaos in the Swift-Hohenberg equation, SIAM Journal on Applied Dynamical Systems, vol.7, issue.3, pp.988-1031, 2008.

N. Yamamoto, A numerical verification method for solutions of boundary value problems with local uniqueness by Banach's fixed-point theorem, SIAM J. Numer. Anal, vol.35, issue.5, pp.2004-2013, 1998.