Interpretation of IEEE-854 floating-point standard and definition in the HOL system, 1995. ,
Basis for the implementation of a reliable dot product, 1992. ,
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
Exponential: implementation trade-offs for hundred bit precision, Real Numbers and Computers, pp.61-74, 2000. ,
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
A floating point technique for extending the available precision, Numerische Mathematik, vol.18, issue.3, pp.224-242, 1971. ,
An Introduction to Numerical Methods and Analysis, 2001. ,
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
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
Accuracy and stability of numerical algorithms, SIAM, 2002. ,
DOI : 10.1137/1.9780898718027
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
Formal verification of a theory of IEEE rounding, 14th International Conference on Theorem Proving in Higher Order Logics, pp.239-254, 2001. ,
How java's floating-point hurts everyone everywhere, ACM 1998 Workshop on Java for High-Performance Network Computing, p.81, 1998. ,
The Art of Computer Programming: Seminumerical Algorithms, 1997. ,
IA-64 and elementary functions: speed and precision, 2000. ,
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=10.1.1.148.9947
Software for Roundoff Analysis, ACM Transactions on Mathematical Software, vol.1, issue.2, pp.108-128, 1975. ,
DOI : 10.1145/355637.355639
Defining the IEEE-854 floating-point standard in PVS, 1995. ,
Elementary functions, algorithms and implementation, 1997. ,
URL : https://hal.archives-ouvertes.fr/ensl-00000008
Numerical Recipes, 1989. ,
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. ,
An American national standard: IEEE standard for binary floating point arithmetic, ACM SIGPLAN Notices, vol.22, issue.2, pp.9-25, 1987. ,
Table-lookup algorithms for elementary functions and their error analysis, Proceedings of the 10th Symposium on Computer Arithmetic, pp.232-236, 1991. ,
Fast hardware-based algorithms for elementary function computations using rectangular multipliers, IEEE Transactions on Computers, vol.43, issue.3, pp.278-294, 1994. ,
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 ,
BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399 ,