M. Jolde? and . Lyon, Rigourous Polynomial Approximations and Applications, 2011.

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.

K. Makino, Rigorous Analysis of Nonlinear Motion in Particle Accelerators, 1998.

N. Brisebarre, M. Jolde?, É. Martin-dorel, M. Mayero, J. Muller et al., Rigorous Polynomial Approximation Using Taylor Models in Coq, NFM'12, ser. LNCS, pp.85-99, 2012.
DOI : 10.1007/978-3-642-28891-3_9
URL : https://hal.archives-ouvertes.fr/ensl-00653460

M. Mayero, Formalisation et automatisation de preuves en analyses réelle et numérique, 2001.

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

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

É. Martin-dorel and E. Lyon, Contributions to the Formal Verification of Arithmetic Algorithms, 2012.
URL : https://hal.archives-ouvertes.fr/tel-00745553

S. Chevillard, J. Harrison, M. Jolde?, 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

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

M. Boespflug, M. Dénès, and B. Grégoire, Full Reduction at Full Throttle, CPP, ser, pp.362-377, 2011.
DOI : 10.1007/3-540-44464-5_13
URL : https://hal.archives-ouvertes.fr/hal-00650940

S. Chevillard, M. Jolde?, and C. Lauter, Sollya: An Environment for the Development of Numerical Codes, Mathematical Software -ICMS 2010, ser. LNCS, pp.28-31, 2010.
DOI : 10.1007/978-3-642-15582-6_5
URL : https://hal.archives-ouvertes.fr/hal-00761644

R. Zumkeller, Formal Global Optimisation with Taylor Models, pp.408-422, 2006.
DOI : 10.1007/11814771_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.680.8497

F. Cháves and . Lyon, Utilisation et certification de l'arithmétique d'intervalles dans un assistant de preuves, 2007.

P. Collins, M. Niqui, and N. , A Validated Real Function Calculus, Mathematics in Computer Science, vol.1, issue.1, pp.437-467, 2011.
DOI : 10.1007/s11786-011-0102-5
URL : https://hal.archives-ouvertes.fr/hal-00641648

A. Solovyev and T. C. Hales, Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations, NFM'13, ser. LNCS, pp.383-397, 2013.
DOI : 10.1007/978-3-642-38088-4_26

J. Harrison, Verifying Nonlinear Real Formulas Via Sums of Squares, TPHOLs, ser. LNCS, pp.102-118, 2007.
DOI : 10.1007/978-3-540-74591-4_9

C. Muñoz and A. Narkawicz, Formalization of Bernstein Polynomials and Applications to Global Optimization, Journal of Automated Reasoning, pp.1-46, 2012.