F. De-dinechin, C. Q. Lauter, and G. Melquiond, Assisted verification of elementary functions using Gappa, Proceedings of the 2006 ACM symposium on Applied computing , SAC '06, pp.1318-1322, 2006.
DOI : 10.1145/1141277.1141584

E. W. Cheney, Introduction to Approximation Theory, 1966.

J. Muller, N. Brisebarre, F. De-dinechin, C. Jeannerod, V. Lefèvre et al., Handbook of Floating-Point Arithmetic, 2009.
DOI : 10.1007/978-0-8176-4705-6

URL : https://hal.archives-ouvertes.fr/ensl-00379167

S. Chevillard, C. Lauter, and M. Joldes, Users' manual for the Sollya tool, Release 2.0, https, 2010.

N. Revol and F. Rouillier, The MPFI library
URL : https://hal.archives-ouvertes.fr/inria-00100985

W. Press, B. Flannery, S. Teukolsky, and W. Vetterling, Numerical recipes: the art of scientific computing, Analytica Chimica Acta, vol.199, 1992.
DOI : 10.1016/S0003-2670(00)82860-3

F. Messine, Méthodes d'optimisation globale basées sur l'analyse d'intervalle pour la résolution deprobì emes avec contraintes, 1997.

R. B. Kearfott, Rigorous Global Search: Continuous Problems, 1996.
DOI : 10.1007/978-1-4757-2495-0

DOI : 10.1016/B978-0-12-505630-4.50021-3

A. Neumaier, Taylor forms ? use and limits, Reliable Computing, vol.9, issue.1, pp.43-79, 2003.
DOI : 10.1023/A:1023061927787

S. Chevillard and C. Lauter, A Certified Infinite Norm for the Implementation of Elementary Functions, Seventh International Conference on Quality Software (QSIC 2007), pp.153-160, 2007.
DOI : 10.1109/QSIC.2007.4385491

URL : https://hal.archives-ouvertes.fr/ensl-00119810

J. Harrison, Floating point verification in HOL light: The exponential function, 1997.
DOI : 10.1007/BFb0000475

K. Makino and M. Berz, Taylor models and other validated functional inclusion methods, International Journal of Pure and Applied Mathematics, vol.4, issue.4, pp.379-456, 2003.

S. Chevillard, M. Joldes, and C. Lauter, Certified and Fast Computation of Supremum Norms of Approximation Errors, 2009 19th IEEE Symposium on Computer Arithmetic, pp.169-176, 2009.
DOI : 10.1109/ARITH.2009.18

URL : https://hal.archives-ouvertes.fr/ensl-00334545

W. Krämer, Sichere und genaue Abschätzung des Approximationsfehlers bei rationalen Approximationen, 1996.

J. Harrison, Verifying Nonlinear Real Formulas Via Sums of Squares, Proc. of the 20th International Conference on Theorem Proving in Higher Order Logics, pp.102-118, 2007.
DOI : 10.1007/978-3-540-74591-4_9

R. E. Moore, Methods and Applications of Interval Analysis, 1979.
DOI : 10.1137/1.9781611970906

M. Berz and K. Makino, COSY INFINITY Version 9

M. Berz and K. Makino, Rigorous global search using taylor models, Proceedings of the 2009 conference on Symbolic numeric computation, SNC '09, pp.11-20, 2009.
DOI : 10.1145/1577190.1577198

M. Berz, K. Makino, and Y. Kim, Long-term stability of the Tevatron by verified global optimization, Nuclear Instruments and Methods in Physics Research Section A: Accelerators , Spectrometers, Detectors and Associated Equipment, proceedings of the 8th International Computational Accelerator Physics Conference -ICAP, pp.1-10, 2004.

F. Rouillier and P. Zimmermann, Efficient isolation of polynomial's real roots, Journal of Computational and Applied Mathematics, vol.162, issue.1, pp.33-50, 2004.
DOI : 10.1016/j.cam.2003.08.015

C. Bendsten and O. Stauning, TADIFF, a Flexible C++ Package for Automatic Differentiation Using Taylor Series, 1997.

A. Griewank, Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation , no. 19 in Frontiers in Appl, Math., SIAM, 2000.
DOI : 10.1137/1.9780898717761

R. P. Brent and H. T. Kung, O((n log n)3/2) ALGORITHMS FOR COMPOSITION AND REVERSION OF POWER SERIES, Analytic Computational Complexity, pp.217-225, 1975.
DOI : 10.1016/B978-0-12-697560-4.50018-6

R. P. Brent and H. T. Kung, Fast Algorithms for Manipulating Formal Power Series, Journal of the ACM, vol.25, issue.4, pp.581-595, 1978.
DOI : 10.1145/322092.322099

L. V. Ahlfors, Complex analysis. An introduction to the theory of analytic functions of one complex variable, 1979.

I. Eble and M. Neher, ACETAF, ACM Transactions on Mathematical Software, vol.29, issue.3, pp.263-286, 2003.
DOI : 10.1145/838250.838252

M. Mezzarobba and B. Salvy, Effective bounds for P-recursive sequences, Journal of Symbolic Computation, vol.45, issue.10, p.arXiv, 2009.
DOI : 10.1016/j.jsc.2010.06.024

URL : https://hal.archives-ouvertes.fr/inria-00376219

K. Makino, Rigorous analysis of nonlinear motion in particle accelerators, 1998.

R. Zumkeller, Global optimization in type theory, Ecole Polytechnique, 2008.

R. Kaivola and M. D. Aagaard, Divider Circuit Verification with Model Checking and Theorem Proving, Theorem Proving in Higher Order Logics: 13th International Conference, pp.338-355, 2000.
DOI : 10.1007/3-540-44659-1_21

J. Harrison, Formal Verification of Floating Point Trigonometric Functions, Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000, pp.217-233, 2000.
DOI : 10.1007/3-540-40922-X_14

R. J. Boulton, Efficiency in a fully-expansive theorem prover, 1994.

M. Blum, Program result checking: A new approach to making programs more reliable, Automata, Languages and Programming, 20th International Colloquium, ICALP93, Proceedings, pp.1-14, 1993.
DOI : 10.1007/3-540-56939-1_57

K. Mehlhorn, S. Neher, M. Seel, R. Seidel, T. Schilz et al., Checking geometric programs or verification of geometric structures, Proceedings of the 12th Annual Symposium on Computational Geometry (FCRC'96), pp.159-165, 1996.

R. Zumkeller, Formal Global Optimization with Taylor Models, Proc. of the 4th International Joint Conference on Automated Reasoning, pp.408-422, 2008.

F. Cháves and M. Daumas, A library of Taylor models for PVS automatic proof checker

H. Ehlich and K. Zeller, Schwankung von Polynomen zwischen Gitterpunkten, Mathematische Zeitschrift, vol.3, issue.1, pp.41-44, 1964.
DOI : 10.1007/BF01111276

P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming, pp.96-293, 2003.
DOI : 10.1007/s10107-003-0387-5

X. Gourdon, Combinatoire, algorithmique et géometrie des polynômes, 1996.

M. Roy, Basic algorithms in real algebraic geometry and their complexity: from Sturm's theorem to the existential theory of reals, of Expositions in Mathematics, de Gruyter Lectures in Real Geometry, 1996.
DOI : 10.1515/9783110811117.1