L. Robert, N. Ashenhurst, and . Metropolis, Unnormalized floating point arithmetic, Journal of the ACM, vol.6, issue.3, pp.415-428, 1959.

A. Avi?ienis, Signed digit number representations for fast parallel arithmetic, IRE Transactions on Electronic Computers, vol.10, pp.389-400, 1961.

G. Bohlender, W. Walter, P. Kornerup, and D. W. Matula, Semantics for exact floating point operations, Proceedings of the 10th Symposium on Computer Arithmetic, pp.22-26, 1991.

S. Boldo and M. Daumas, Faithful rounding without fused multiply and accumulate, IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, 2002.

S. Boldo and M. Daumas, Properties of the subtraction valid for any floating point system, 7th International Workshop on Formal Methods for Industrial Critical Systems, pp.137-149, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00072115

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

W. J. Cody and R. Karpinski, A proposed radix and word-length independent standard for floating point arithmetic, IEEE Micro, vol.4, issue.4, pp.86-100, 1984.

J. T. Coonen, Specification for a proposed standard for floating point arithmetic. Memorandum ERL M78/72, 1978.

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.

M. Daumas, L. Rideau, and L. Théry, A generic library of floating-point numbers and its application to exact computing, 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001.

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

J. Harrison, A machine-checked theory of floating point arithmetic, 12th International Conference on Theorem Proving in Higher Order Logics, pp.113-130, 1999.

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq proof assistant: a tutorial: version 7.2, 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, Further remarks on reducing truncation errors, Communications of the ACM, vol.8, issue.1, p.40, 1965.

A. H. Karp and P. Markstein, High precision division and square root, ACM Transactions on Mathematical Software, vol.23, issue.4, pp.561-589, 1997.

D. E. Knuth, The art of computer programming: Seminumerical Algorithms, 1969.

S. Linnainmaa, Analysis of some known methods of improving the accuracy of floating-point sums, BIT, vol.14, pp.167-202, 1974.

S. Linnainmaa, Software for doubled precision floating point computations, ACM Transactions on Mathematical Software, vol.7, issue.3, pp.272-283, 1981.

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

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

O. Møller, Note on quasi double-precision, vol.BIT, pp.251-255, 1965.

O. Møller, Quasi double-precision in floating point addition, BIT, vol.5, issue.1, pp.37-50, 1965.

M. Pichat and J. Vignes, Ingénierie du contrôle de la précision des calculs sur ordinateur, 1993.

F. John, D. E. Reiser, and . Knuth, Evading the drift in floating point addition, Information Processing Letters, vol.3, issue.3, pp.84-87, 1975.

J. Rushby and . Friedrich-von-henke, Formal verification of algorithms for critical systems, Proceedings of the Conference on Software for Critical Systems, pp.1-15, 1991.

D. M. 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.

J. R. Shewchuk, Adaptive precision floating-point arithmetic and fast robust geometric predicates, Discrete and Computational Geometry, vol.18, pp.305-363, 1997.

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

, Texas Instruments. TMS320C3x -User's guide, 1997.

W. G. Wadey, End MOMR. INRIA Unité de recherche INRIA Rhône-Alpes 655, avenue de l'Europe -38330 Montbonnot, Journal of the ACM, vol.7, issue.2, pp.129-139, 1960.

. Unité-de-recherche-inria-futurs, Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche INRIA Lorraine : LORIA, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602