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

D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-47, 1991.
DOI : 10.1145/103162.103163

R. E. Moore, Interval analysis, 1966.

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

F. De-dinechin, A. Ershov, and N. Gast, Towards the postultimate libm, 17th IEEE Symposium on Computer Arithmetic, pp.288-295, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070636

F. De-dinechin, C. Q. Lauter, and J. Muller, Fast and correctly rounded logarithms in double-precision, Theoretical Informatics and Applications, pp.85-102, 2007.
DOI : 10.1051/ita:2007003
URL : https://hal.archives-ouvertes.fr/inria-00070331

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

T. J. Dekker, A floating-point technique for extending the available precision, Numerische Mathematik, vol.5, issue.3, pp.224-242, 1971.
DOI : 10.1007/BF01397083

D. Knuth, The Art of Computer Programming, Seminumerical Algorithms, 1997.

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Theorem Proving in Higher Order Logics: 14th International Conference, pp.169-184, 2001.
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285

S. Gal, Computing elementary functions: A new approach for achieving high accuracy and good performance, Accurate Scientific Computations, ser, pp.1-16, 1986.
DOI : 10.1007/3-540-16798-6_1

P. T. Tang, Table-lookup algorithms for elementary functions and their error analysis, [1991] Proceedings 10th IEEE Symposium on Computer Arithmetic, 1991.
DOI : 10.1109/ARITH.1991.145565

S. Story and P. Tang, New algorithms for improved transcendental functions on IA-64, Proceedings 14th IEEE Symposium on Computer Arithmetic (Cat. No.99CB36336), pp.4-11, 1999.
DOI : 10.1109/ARITH.1999.762822

R. Li, P. Markstein, J. P. Okada, and J. W. Thomas, The libm library and floating-point arithmetic for HP-UX on Itanium, 2001.

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

D. Priest, Fast table-driven algorithms for interval elementary functions, Proceedings 13th IEEE Sympsoium on Computer Arithmetic, pp.168-174, 1997.
DOI : 10.1109/ARITH.1997.614892

P. Markstein, IA-64 and Elementary Functions: Speed and Precision, ser. Hewlett-Packard Professional Books, 2000.

S. Chevillard, C. Lauter, and M. Jolde¸sjolde¸s, 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

S. Chevillard, J. Harrison, M. Jolde¸sjolde¸s, C. Lauter, C. /. Ens-lyon et al., Efficient and accurate computation of upper bounds of approximation errors, CACAO project and Intel Corporation, 2010.
DOI : 10.1016/j.tcs.2010.11.052
URL : https://hal.archives-ouvertes.fr/ensl-00445343

P. H. Sterbenz, Floating point computation, 1974.

F. De-dinechin and S. Maidanov, Software techniques for perfect elementary functions in floating-point interval arithmetic, 7th Conference on Real Numbers and Computers, 2006.

J. Harrison, Formal Verification of Square Root Algorithms, Formal Methods in System Design, vol.22, issue.2, pp.143-153, 2003.
DOI : 10.1023/A:1022973506233

W. Hofschuster and W. Krämer, FI_LIB, eine schnelle und portable Funktionsbibliothek für reelle Argumente und reelle Intervalle im IEEE-double-Format, Institut für Wissenschaftliches Rechnen und Mathematische Modellbildung, 1998.

M. Lerch, G. Tischler, J. W. Von-gudenberg, W. Hofschuster, and W. Krämer, FILIB++, a fast interval library supporting containment computations, ACM Transactions on Mathematical Software, vol.32, issue.2, pp.299-324, 2006.
DOI : 10.1145/1141885.1141893

M. Daumas and G. Melquiond, Generating formally certified bounds on values and round-off errors, 6th Conference on Real Numbers and Computers, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00070739

G. Melquiond and S. Pion, Formally certified floating-point filters for homogeneous geometric predicates, Theoretical Informatics and Applications, pp.57-70, 2007.
DOI : 10.1051/ita:2007005
URL : https://hal.archives-ouvertes.fr/inria-00071232

S. Boutin, Using reflection to build efficient and certified decision procedures, Third International Symposium on Theoretical Aspects of Computer Software, pp.515-529, 1997.
DOI : 10.1007/BFb0014565

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq proof assistant: a tutorial: version 8.0, 2004.

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

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, 11th International Conference on Automated Deduction, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

I. Iec, I. Standard, and I. Iec, (E) Programming languages ? C, p.1999, 1999.

F. De-dinechin, C. Q. Lauter, and G. Melquiond, Assisted verification of elementary functions, LIP, Tech. Rep, pp.2005-2048, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070330

C. Q. Lauter and F. De-dinechin, Optimising polynomials for floating-point implementation, 8th Conference on Real Numbers and Computers, pp.7-16, 2008.