D. Bini, Y. Victor, and . Pan, Polynomial and Matrix Computations: Fundamental Algorithms, 1994.

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.

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

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

N. J. Higham, Accuracy and stability of numerical algorithms. SIAM, 2002.

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 and J. D. Darcy, How java's floating-point hurts everyone everywhere, ACM 1998 Workshop on Java for High-Performance Network Computing, vol.81, 1998.

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

, Ropp (powerRZ radix (Zpred (Zpred (Zopp (dExp b

, // Set the residual error Err0 = 0

, // Set the range for the indeterminate XMax

=. Errx and . Ulpieee, XMax

/. , Test the criterion HornerAXPY, issue.0

. &lt;&lt;-&quot;result, << rec_erreur <<, << rec_check << endl

, All the steps of Horner's rule were faithful\n, == 0.0) cout <<

, else if (rec_check < 1.0) cout << "The final step of Horner's rule was faithful\n

, else if (rec_check >= 1.0) cout << "Error too large to guarantee that Horner's rule was faithful\n

. }-//, A simple JAVA test qualifying the accuracy of Horner's rule for polynomials

, // Formulas are part of the graduate work of Sylvie BOLDO, 2001.

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

, Lesser General Public // License along with this library; if not, Suite, vol.330, pp.2111-1307

, class Horner { public static double

, public static double UlpCstIEEE

, public static void main(String[] args) { int lgfr

, Omitted messages

. //-initialize, Ulp for (UlpCstIEEE = 1.0, lgfr = 52; lgfr > 0

, // Enter the polynomial Coefficients = new double, vol.9