A. Victor and . Carreño, Interpretation of IEEE-854 floating-point standard and definition in the HOL system, 1995.

M. Daumas, Basis for the implementation of a reliable dot product, 1992.

M. Daumas and D. W. Matula, Validated roundings of dot products by sticky accumulation, IEEE Transactions on Computers, vol.46, issue.5, pp.623-629, 1997.
DOI : 10.1109/12.589241

M. Daumas and C. Moreau-finot, Exponential: implementation trade-offs for hundred bit precision, Real Numbers and Computers, pp.61-74, 2000.

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

URL : https://hal.archives-ouvertes.fr/hal-00157285

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

J. F. Epperson, An Introduction to Numerical Methods and Analysis, 2001.

C. T. Fike, Methods of evaluating polynomial approximations in function evaluation routines, Communications of the ACM, vol.10, issue.3, pp.175-178, 1967.
DOI : 10.1145/363162.363200

J. Harrison, A Machine-Checked Theory of Floating Point Arithmetic, 12th International Conference on Theorem Proving in Higher Order Logics, pp.113-130, 1999.
DOI : 10.1007/3-540-48256-3_9

N. J. Higham, Accuracy and stability of numerical algorithms, SIAM, 2002.
DOI : 10.1137/1.9780898718027

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq proof assistant: a tutorial: version 7.2, Institut National de Recherche en Informatique et en Automatique, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00069918

C. Jacobi, Formal verification of a theory of IEEE rounding, 14th International Conference on Theorem Proving in Higher Order Logics, pp.239-254, 2001.

W. Kahan and J. D. Darcy, How java's floating-point hurts everyone everywhere, ACM 1998 Workshop on Java for High-Performance Network Computing, p.81, 1998.

E. Donald and . Knuth, The Art of Computer Programming: Seminumerical Algorithms, 1997.

P. Markstein, IA-64 and elementary functions: speed and precision, 2000.

W. Miller, Computational complexity and numerical stability, Proceedings of the 6th ACM Symposium of the Theory Of Computation, pp.317-322, 1974.
DOI : 10.1145/800119.803910

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

W. Miller, Software for Roundoff Analysis, ACM Transactions on Mathematical Software, vol.1, issue.2, pp.108-128, 1975.
DOI : 10.1145/355637.355639

P. S. Miner, Defining the IEEE-854 floating-point standard in PVS, 1995.

J. Muller, Elementary functions, algorithms and implementation, 1997.
URL : https://hal.archives-ouvertes.fr/ensl-00000008

H. William, B. P. Press, S. A. Flannery, W. T. Teukolsky, and . Vetterling, Numerical Recipes, 1989.

M. David and . Russinoff, A mechanically checked proof of IEEE compliance of the floating point multiplication , division and square root algorithms of the AMD-K7 processor, LMS Journal of Computation and Mathematics, vol.1, pp.148-200, 1998.

N. L. Schryer, A test of computer's floating-point arithmetic unit, 1981.

D. Stevenson, An American national standard: IEEE standard for binary floating point arithmetic, ACM SIGPLAN Notices, vol.22, issue.2, pp.9-25, 1987.

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

W. Fai, W. , 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.

I. Unité-de-recherche and . Futurs, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rocquencourt, Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche INRIA Sophia Antipolis : 2004, route des Lucioles -BP 93 -06902 Sophia Antipolis Cedex, pp.105-78153

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399