Unnormalized floating point arithmetic, Journal of the ACM, vol.6, issue.3, pp.415-428, 1959. ,
Signed digit number representations for fast parallel arithmetic, IRE Transactions on Electronic Computers, vol.10, pp.389-400, 1961. ,
Semantics for exact floating point operations, Proceedings of the 10th Symposium on Computer Arithmetic, pp.22-26, 1991. ,
Faithful rounding without fused multiply and accumulate, IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, 2002. ,
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
Interpretation of IEEE-854 floating-point standard and definition in the HOL system, 1995. ,
A proposed radix and word-length independent standard for floating point arithmetic, IEEE Micro, vol.4, issue.4, pp.86-100, 1984. ,
Specification for a proposed standard for floating point arithmetic. Memorandum ERL M78/72, 1978. ,
Validated roundings of dot products by sticky accumulation, IEEE Transactions on Computers, vol.46, issue.5, pp.623-629, 1997. ,
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. ,
A floating point technique for extending the available precision, Numerische Mathematik, vol.18, issue.3, pp.224-242, 1971. ,
A machine-checked theory of floating point arithmetic, 12th International Conference on Theorem Proving in Higher Order Logics, pp.113-130, 1999. ,
The Coq proof assistant: a tutorial: version 7.2, 2002. ,
URL : https://hal.archives-ouvertes.fr/inria-00069918
Formal verification of a theory of IEEE rounding, 14th International Conference on Theorem Proving in Higher Order Logics, pp.239-254, 2001. ,
Further remarks on reducing truncation errors, Communications of the ACM, vol.8, issue.1, p.40, 1965. ,
High precision division and square root, ACM Transactions on Mathematical Software, vol.23, issue.4, pp.561-589, 1997. ,
The art of computer programming: Seminumerical Algorithms, 1969. ,
Analysis of some known methods of improving the accuracy of floating-point sums, BIT, vol.14, pp.167-202, 1974. ,
Software for doubled precision floating point computations, ACM Transactions on Mathematical Software, vol.7, issue.3, pp.272-283, 1981. ,
IA-64 and elementary functions: speed and precision, 2000. ,
Defining the IEEE-854 floating-point standard in PVS, 1995. ,
Note on quasi double-precision, vol.BIT, pp.251-255, 1965. ,
Quasi double-precision in floating point addition, BIT, vol.5, issue.1, pp.37-50, 1965. ,
Ingénierie du contrôle de la précision des calculs sur ordinateur, 1993. ,
Evading the drift in floating point addition, Information Processing Letters, vol.3, issue.3, pp.84-87, 1975. ,
Formal verification of algorithms for critical systems, Proceedings of the Conference on Software for Critical Systems, pp.1-15, 1991. ,
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. ,
A test of computer's floating-point arithmetic unit, 1981. ,
Adaptive precision floating-point arithmetic and fast robust geometric predicates, Discrete and Computational Geometry, vol.18, pp.305-363, 1997. ,
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.
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. ,
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 ,