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

A. Benoit, M. Jolde?, and M. Mezzarobba, Rigorous uniform approximation of D-finite 719 functions using Chebyshev expansions, Math. Comp, vol.86, issue.305, pp.1303-1341, 2017.

V. Berinde, Iterative approximation of fixed points, volume 1912 of Lecture Notes in Mathem-721 atics, 2007.

M. Berz and K. Makino, Verified integration of odes and flows using differential algebraic 723 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 725

, Lax-Milgram theorem, Proc. 6th ACM SIGPLAN Conference on Certified Programs and 726 Proofs, 2017.

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

N. Bourbaki, General Topology, p.730, 1995.

. Paris, , 1971.

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

. Software, , 2018.

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

N. Brisebarre and M. Jolde?, Chebyshev interpolation polynomial-based tools for rigorous 737 computing, Proc. Proceedings of the 2010 International Symposium on Symbolic and 738 Algebraic Computation, pp.147-154, 2010.

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

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

T. A. Driscoll, N. Hale, and L. N. Trefethen, Chebfun guide, 2014.

L. Fox and I. B. Parker, Chebyshev polynomials in numerical analysis, Oxford University, p.745

B. Grégoire and L. Théry, A purely functional library for modular arithmetic and its application 747 to certifying large prime numbers, Proc. Automated Reasoning, Third International Joint, p.748

, Proceedings, vol.4130, p.749, 2006.

, Lecture Notes in Computer Science, pp.423-437, 2006.

T. C. Hales, M. Adams, G. Bauer, D. T. Dang, J. Harrison et al., , p.751

V. Magron, S. Mclaughlin, T. T. Nguyen, T. Q. Nguyen, T. Nipkow et al., , p.752

J. Rute, A. Solovyev, A. H. Ta, T. N. Tran, D. T. Trieu et al., , p.754, 2015.

J. Hölzl, F. Immler, and B. Huffman, Type classes and filters for mathematical analysis in 755

, Interactive Theorem, p.756

. Proving, , pp.279-294, 2013.

A. Hungria, J. Lessard, and J. D. Mireles-james, Rigorous numerics for analytic solutions 758 of differential equations: the radii polynomial approach, Math. Comp, vol.85, issue.299, p.759

F. Immler, A verified ODE solver and the Lorenz attractor, vol.761, pp.1-39, 2018.

F. Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic, IEEE 763 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, p.765, 2011.

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

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

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

J. Lessard and C. Reinhardt, Rigorous numerics for nonlinear differential equations using 772 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 774 integrals, Journal of Automated Reasoning, vol.62, issue.2, pp.281-300, 2019.

É. Martin-dorel and G. Melquiond, Proving tight bounds on univariate expressions with 776 elementary functions in coq, Journal of Automated Reasoning, vol.57, issue.3, pp.187-217, 2016.

G. Melquiond, Proving bounds on real-valued functions with computations, Proc. Interna-778 tional 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 781 mpfi library, Reliable computing, vol.11, issue.4, pp.275-290, 2005.

S. M. Rump, Intlab-interval laboratory, Developments in reliable computing, pp.77-104

. Springer, , 1999.

L. N. Trefethen, Approximation Theory and Approximation Practice. SIAM, 2013.

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

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

J. B. Van-den, J. Berg, and . Lessard, Chaotic braided solutions via rigorous numerics: Chaos 791 in the Swift-Hohenberg equation, SIAM Journal on Applied Dynamical Systems, vol.7, issue.3, p.792

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