. Cr-libm,

, Standard 754-1985 for binary floating-point arithmetic (also IEC 60559), 1985.

Y. Bertot and P. Casteran, Coq'Art: the Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

M. Cornea, J. Harrison, and P. T. Tang, Scientific Computing on Itanium-based Systems, 2002.

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

D. Defour, Cache-optimised methods for the evaluation of elementary functions, 2002.
URL : https://hal.archives-ouvertes.fr/hal-02102051

F. De-dinechin and D. Defour, Software carry-save: A case study for instruction-level parallelism, Seventh International Conference on Parallel Computing Technologies, 2003.

F. De-dinechin, D. Defour, and C. Q. Lauter, Fast correct rounding of elementary functions in double precision using double-extended arithmetic, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00071446

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

F. De-dinechin, C. Loirat, and J. Muller, A proven correctly rounded logarithm in doubleprecision, RNC6, Real Numbers and Computers, 2004.

D. Defour, Collapsing dependent floating point operations, 2004.

D. Defour and F. De-dinechin, Software carry-save for fast multiple-precision algorithms, 35th International Congress of Mathematical Software, 2002.
URL : https://hal.archives-ouvertes.fr/hal-02102038

D. Defour, F. De-dinechin, and J. Muller, Correctly rounded exponential function in double precision arithmetic, Advanced Signal Processing Algorithms, Architectures, and Implementations X (SPIE'2000), 2001.
URL : https://hal.archives-ouvertes.fr/inria-00072387

T. J. Dekker, A floating point technique for extending the available precision, Numerische Mathematik, vol.18, issue.3, pp.224-242, 1971.

P. M. Farmwald, High bandwidth evaluation of elementary functions, Proceedings of the 5th IEEE Symposium on Computer Arithmetic. IEEE, 1981.

S. , Computing elementary functions: A new approach for achieving high accuracy and good performance, Accurate Scientific Computations, vol.235, pp.1-16, 1986.

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

W. Hofschuster and W. Krämer, FI LIB, eine schnelle und portable Funktionsbibliothek für reelle Argumente und reelle Intervalle im IEEE-double-Format, 1998.

. Iso/iec, International Standard ISO/IEC 9899:1999(E), 1999.

R. Klatte, U. Kulisch, C. Lawo, M. Rauch, and A. Wiethoff, C-XSC a C++ class library for extended scientific computing, 1993.

V. Lefèvre, Moyens arithmétiques pour un calcul fiable, 2000.

V. Lefèvre and J. Muller, Worst cases for correct rounding of the elementary functions in double precision, 2004.

V. Lefèvre, J. M. Muller, and A. Tisserand, Towards correctly rounded transcendentals, IEEE Transactions on Computers, vol.47, issue.11, pp.1235-1243, 1998.

. Ibm-accurate-portable and . Mathlib,

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

R. E. Moore, Interval analysis, 1966.

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

P. T. Tang, Table lookup algorithms for elementary functions and their error analysis, Proceedings of the 10th IEEE Symposium on Computer Arithmetic, pp.232-236, 1991.

W. F. Wong and E. Goto, Fast hardware-based algorithms for elementary function computations using rectangular multipliers, IEEE Transactions on Computers, vol.43, issue.3, pp.278-294, 1994.

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.

, Unité de recherche INRIA Rhône-Alpes 655, avenue de l'Europe -38334 Montbonnot

. Unité-de-recherche-inria-futurs, Parc Club Orsay Université -ZAC des Vignes 4, rue Jacques Monod -91893 ORSAY Cedex

. Unité-de-recherche-inria-lorraine, LORIA, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602