B. Akbarpour and L. C. Paulson, MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions, Journal of Automated Reasoning, vol.7, issue.4, pp.175-205, 2010.
DOI : 10.1007/s10817-009-9149-2

X. Allamigeon, S. Gaubert, V. Magron, and B. Werner, Certification of Bounds of Non-linear Functions: The Templates Method, Intelligent Computer Mathematics -MKM, Calculemus, DML, and Systems and Projects, pp.51-65978, 2013.
DOI : 10.1007/978-3-642-39320-4_4
URL : https://hal.archives-ouvertes.fr/hal-00932333

S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011.
DOI : 10.1109/ARITH.2011.40
URL : https://hal.archives-ouvertes.fr/inria-00534854

N. Brisebarre, M. Jolde¸sjolde¸s, É. Martin-dorel, M. Mayero, J. M. Muller et al., Rigorous Polynomial Approximation Using Taylor Models in Coq, Proceedings of 4th International Symposium on NASA Formal Methods, pp.85-99, 2012.
DOI : 10.1007/978-3-642-28891-3_9
URL : https://hal.archives-ouvertes.fr/ensl-00653460

M. Ceberio and L. Granvilliers, Horner's rule for interval evaluation revisited, Computing, vol.69, issue.1, pp.51-81, 2002.
DOI : 10.1007/s00607-002-1448-y

S. Chevillard, J. Harrison, M. Jolde¸sjolde¸s, and C. Lauter, Efficient and accurate computation of upper bounds of approximation errors, Theoretical Computer Science, vol.412, issue.16, pp.1523-1543, 2011.
DOI : 10.1016/j.tcs.2010.11.052
URL : https://hal.archives-ouvertes.fr/ensl-00445343

S. Chevillard, M. Jolde¸sjolde¸s, and C. Lauter, Sollya: An Environment for the Development of Numerical Codes, Proceedings of the 3rd International Congress on Mathematical Software, pp.28-31, 2010.
DOI : 10.1007/978-3-642-15582-6_5
URL : https://hal.archives-ouvertes.fr/hal-00761644

M. Daumas, D. Lester, and C. Muñoz, Verified Real Number Calculations: A Library for Interval Arithmetic, IEEE Transactions on Computers, vol.58, issue.2, pp.226-237, 2009.
DOI : 10.1109/TC.2008.213
URL : https://hal.archives-ouvertes.fr/hal-00168402

M. Daumas, G. Melquiond, and C. Muñoz, Guaranteed Proofs Using Interval Arithmetic, 17th IEEE Symposium on Computer Arithmetic (ARITH'05), pp.188-195
DOI : 10.1109/ARITH.2005.25
URL : https://hal.archives-ouvertes.fr/hal-00164621

W. Denman and C. Muñoz, Automated Real Proving in PVS via MetiTarski, FM, Lecture Notes in Computer Science, pp.194-199, 2014.
DOI : 10.1007/978-3-319-06410-9_14

E. Hansen and G. Walster, Global Optimization Using Interval Analysis: Revised And Expanded. Monographs and textbooks in pure and applied mathematics, 2003.

J. Harrison, Verifying the accuracy of polynomial approximations in HOL, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, pp.137-152, 1007.
DOI : 10.1007/BFb0028391

J. Harrison, Verifying Nonlinear Real Formulas Via Sums of Squares, Proceedings 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

M. Jolde¸sjolde¸s and F. Ens-de-lyon, Rigorous Polynomial Approximations and applications, 2011.

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

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.

É. Martin-dorel, M. Mayero, I. Pa¸scapa¸sca, L. Rideau, and L. Théry, Certified, Efficient and Sharp Univariate Taylor Models in COQ, 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp.193-200, 2013.
DOI : 10.1109/SYNASC.2013.33
URL : https://hal.archives-ouvertes.fr/hal-00845791

G. Melquiond, Floating-point arithmetic in the Coq system, Proceedings of the 8th Conference on Real Numbers and Computers, pp.93-102, 2008.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913

G. Melquiond, Proving Bounds on Real-Valued Functions with Computations, Proceedings of the 4th International Joint Conference on Automated Reasoning, pp.2-17, 2008.
DOI : 10.1007/978-3-540-71070-7_2
URL : https://hal.archives-ouvertes.fr/hal-00180138

G. Melquiond, Floating-point arithmetic in the Coq system, Information and Computation, vol.216, pp.14-23, 2012.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913

R. E. Moore, Interval Analysis, 1966.

J. M. Muller, N. Brisebarre, F. De-dinechin, C. P. Jeannerod, V. Lefèvre et al., Handbook of Floating-Point Arithmetic, Birkhäuser Boston, pp.978-978, 2010.
DOI : 10.1007/978-0-8176-4705-6
URL : https://hal.archives-ouvertes.fr/ensl-00379167

C. Muñoz and A. Narkawicz, Formalization of Bernstein Polynomials and Applications to Global Optimization, Journal of Automated Reasoning, vol.43, issue.1, pp.151-196, 1007.
DOI : 10.1007/s10817-012-9256-3

A. Narkawicz and C. Muñoz, A Formally Verified Generic Branching Algorithm for Global Optimization, Proceedings of the 5th International Conference on Verified Software: Theories, Tools, Experiments, pp.326-343978, 2013.
DOI : 10.1007/978-3-642-54108-7_17

A. Solovyev and T. C. Hales, Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations, Proceedings of the 5th International Symposium on NASA Formal Methods, pp.383-397978, 2013.
DOI : 10.1007/978-3-642-38088-4_26

P. T. Tang, Table-driven implementation of the exponential function in IEEE floating-point arithmetic, ACM Transactions on Mathematical Software, vol.15, issue.2, pp.144-157, 1989.
DOI : 10.1145/63522.214389

A. Ziv, Fast evaluation of elementary mathematical functions with correctly rounded last bit, ACM Transactions on Mathematical Software, vol.17, issue.3, pp.410-423, 1991.
DOI : 10.1145/114697.116813

R. Zumkeller, Global Optimization in Type Theory, France, 2008.