M. Abramowitz and I. A. Stegun, Handbook of mathematical functions with formulas, graphs, and mathematical tables For sale by the Superintendent of Documents, National Bureau of Standards Applied Mathematics Series U.S. Government Printing Office, vol.55, 1964.

M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, ITP. LNCS, pp.83-98, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496

A. Benoit, F. Chyzak, A. Darrasse, S. Gerhold, M. Mezzarobba et al., The Dynamic Dictionary of Mathematical Functions (DDMF), Mathematical Software -ICMS 2010, pp.35-41, 2010.
DOI : 10.1007/978-3-642-15582-6_7
URL : https://hal.archives-ouvertes.fr/hal-00783048

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

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
DOI : 10.1145/1577190.1577198

M. Berz, K. Makino, and Y. K. 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.

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

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 and S. Chevillard, Efficient polynomial L-approximations, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.169-176, 2007.
DOI : 10.1109/ARITH.2007.17
URL : https://hal.archives-ouvertes.fr/inria-00119513

N. Brisebarre, J. M. Muller, and A. Tisserand, Computing machine-efficient polynomial approximations, ACM Transactions on Mathematical Software, vol.32, issue.2, pp.236-256, 2006.
DOI : 10.1145/1141885.1141890
URL : https://hal.archives-ouvertes.fr/ensl-00086826

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

S. Chevillard, Évaluation efficace de fonctions numériques Outils et exemples, 2009.

S. Chevillard, M. Jolde?, C. Lauter, K. Fukuda, J. Van-der-hoeven et al., Sollya: An Environment for the Development of Numerical Codes, Mathematical Software -ICMS 2010, pp.28-31, 2010.
DOI : 10.1007/978-3-642-15582-6_5
URL : https://hal.archives-ouvertes.fr/hal-00761644

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

P. Collins, M. Niqui, and N. Revol, A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq, NSV-3: Third International Workshop on Numerical Software Verification, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00473270

F. De-dinechin, C. Lauter, G. Melquiond, J. Zur-gathen, and J. Gerhard, Assisted verification of elementary functions using Gappa Modern computer algebra, Proceedings of the 2006 ACM Symposium on Applied Computing, pp.1318-1322, 2003.

H. Geuvers and M. Niqui, Constructive Reals in Coq: Axioms and Categoricity, Proceedings of TYPES 2000, pp.79-95, 2002.
DOI : 10.1007/3-540-45842-5_6

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

B. Grégoire and L. Théry, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, IJCAR. LNCS, pp.423-437, 2006.
DOI : 10.1007/11814771_36

A. Griewank, Evaluating Derivatives -Principles and Techniques of Algorithmic Differentiation, SIAM, 2000.

M. Jolde?, Rigourous Polynomial Approximations and Applications. Ph.D. dissertation , École Normale Supérieure de Lyon, 2011.

R. Krebbers and B. Spitters, Computer Certified Efficient Exact Reals in Coq, pp.90-106, 2011.
DOI : 10.1007/978-3-642-04027-6_12

V. Lefèvre and J. M. Muller, Worst cases for correct rounding of the elementary functions in double precision, Proceedings 15th IEEE Symposium on Computer Arithmetic. ARITH-15 2001, 2001.
DOI : 10.1109/ARITH.2001.930110

P. D. Lizia, Robust Space Trajectory and Space System Design using Differential Algebra, 2008.

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.

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

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

R. E. Moore, Methods and Applications of Interval Analysis, Society for Industrial and Applied Mathematics, 1979.
DOI : 10.1137/1.9781611970906

J. M. Muller, Projet ANR TaMaDi ? Dilemme du fabricant de tables ? Table Maker's Dilemma (ref. ANR, 2010.

J. M. Muller, Elementary Functions, Algorithms and Implementation, 2006.
URL : https://hal.archives-ouvertes.fr/ensl-00000008

M. Neher, K. R. Jackson, and N. S. Nedialkov, On Taylor Model Based Integration of ODEs, SIAM Journal on Numerical Analysis, vol.45, issue.1, pp.236-262, 2007.
DOI : 10.1137/050638448

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

O. Connor and R. , Certified exact transcendental real number computation in coq, Theorem Proving in Higher Order Logics, pp.246-261, 2008.

T. A. Project, CRlibm, Correctly Rounded mathematical library, 2006.

E. Remez, Sur un procédé convergent d'approximations successives pour déterminer les polynômes d'approximation (in French), C.R. Académie des Sciences, pp.2063-2065, 1934.

B. Salvy and P. Zimmermann, GFUN: a Maple package for the manipulation of generating and holonomic functions in one variable, ACM Transactions on Mathematical Software, vol.20, issue.2, pp.163-177, 1994.
DOI : 10.1145/178365.178368
URL : https://hal.archives-ouvertes.fr/hal-00917741

R. P. Stanley, Differentiably Finite Power Series, European Journal of Combinatorics, vol.1, issue.2, pp.175-188, 1980.
DOI : 10.1016/S0195-6698(80)80051-5
URL : http://doi.org/10.1016/s0195-6698(80)80051-5

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, Formal Global Optimization with Taylor Models, Proc. of the 4th International Joint Conference on Automated Reasoning, pp.408-422, 2008.
DOI : 10.1007/11814771_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.680.8497