. Ce-document-ne-constitue and . Qu, Voici une sélection de quelques ouvrages pour creuser certains des sujets abordés Concernant l'arithmétique à virgule flottante au sens de la norme IEEE-754 et ses utilisations avancées , l'ouvrage de référence est Handbook of Floating-Point Arithmetic [37]. Pour avoir plus de détails sur la façon dont elle est implantée efficacement en matériel, consultez Digital Arithmetic [20]. De plus amples informations sur le calcul en précision plus haute que celle fournie par le matériel se trouvent dans cet article dédié à la géométrie algorithmique : Adaptative precision floating-point arithmetic and fast robust geometric predicates [40]. Quant aux algorithmes pour faire du calcul efficace multi-précision en général, l'ouvrage de référence est Modern Computer Arithmetic [13], bon ouvrage sur ces deux sujets est Accuracy and Stability of Numerical Algorithms

. Enfin, arithmétique à virgule flottante, on pourra lire cette version longue d'un article dédié à la vérification de bout en bout d'une fonction élémentaire en HOL Light : Floating-point verification in HOL Light: the exponential function [22]. Pour ce qui est de l'utilisation de Coq pour la preuve de propriété an arithmétique flottante, se reporter à la thèse Preuves formelles en arithmétiques à virgule flottante

S. Boldo, Preuves formelles en arithmétiques à virgule flottante, 2004.

S. Boldo, Floats and Ropes: A Case Study for Formal Numerical Program Verification, Proceedings of the 36th International Colloquium on Automata, Languages and Programming, pp.91-102, 2009.
DOI : 10.1007/978-3-642-02930-1_8

S. Boldo, Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven, IEEE Transactions on Computers, vol.58, issue.2, pp.220-225, 2009.
DOI : 10.1109/TC.2008.200

S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Formal Proof of a Wave Equation Resolution Scheme: The Method Error, Proceedings of the first Interactive Theorem Proving Conference, pp.147-162, 2010.
DOI : 10.1007/978-3-642-14052-5_12
URL : https://hal.archives-ouvertes.fr/inria-00450789

S. Boldo and M. Daumas, A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials, Numerical Algorithms, vol.37, issue.1-4, pp.45-60, 2004.
DOI : 10.1023/B:NUMA.0000049487.98618.61

S. Boldo, J. Filliâtre, and G. Melquiond, Combining Coq and Gappa for Certifying Floating-Point Programs, Proceedings of the 16th Calculemus Symposium, pp.59-74, 2009.
DOI : 10.1109/TC.2008.200
URL : https://hal.archives-ouvertes.fr/inria-00432726

S. Boldo and G. Melquiond, Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd, IEEE Transactions on Computers, vol.57, issue.4, pp.462-471, 2008.
DOI : 10.1109/TC.2007.70819
URL : https://hal.archives-ouvertes.fr/inria-00080427

S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011.
DOI : 10.1109/ARITH.2011.40
URL : https://hal.archives-ouvertes.fr/inria-00534854

S. Boldo and J. Muller, Exact and Approximated Error of the FMA, IEEE Transactions on Computers, vol.60, issue.2, pp.157-164, 2011.
DOI : 10.1109/TC.2010.139
URL : https://hal.archives-ouvertes.fr/inria-00429617

S. Boldo and C. Muñoz, Provably faithful evaluation of polynomials, Proceedings of the 2006 ACM symposium on Applied computing , SAC '06, pp.1328-1332, 2006.
DOI : 10.1145/1141277.1141586
URL : https://hal.archives-ouvertes.fr/inria-00000892

S. Boldo, T. M. , and T. Nguyen, Proofs of numerical programs when the compiler optimizes, Innovations in Systems and Software Engineering, pp.1-10, 2011.
DOI : 10.1007/s11334-011-0151-6
URL : https://hal.archives-ouvertes.fr/hal-00777639

P. Richard, P. Brent, and . Zimmermann, Modern Computer Arithmetic, 2010.

M. Cornea, C. Iordache, J. Harrison, and P. Markstein, Integer divide and remainder operations in the IA-64 architecture, Proceedings of the 4th Conference on Real Numbers and Computers, pp.161-184, 2000.

M. Daumas and G. Melquiond, Certification of bounds on expressions involving rounded operators, ACM Transactions on Mathematical Software, vol.37, issue.1, 2010.
DOI : 10.1145/1644001.1644003
URL : https://hal.archives-ouvertes.fr/hal-00127769

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Proceedings of the 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

C. Florent-de-dinechin, G. Lauter, and . Melquiond, Certifying the Floating-Point Implementation of an Elementary Function Using Gappa, IEEE Transactions on Computers, vol.60, issue.2, pp.242-253, 2011.
DOI : 10.1109/TC.2010.128

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

W. Edsger and . Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.

D. Milo?, T. Ercegovac, and . Láng, Digital Arithmetic, 2004.

D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-47, 1991.
DOI : 10.1145/103162.103163

J. Harrison, Floating point verification in HOL light: The exponential function, 1997.
DOI : 10.1007/BFb0000475

J. Harrison, Formal Verification of IA-64 Division Algorithms, Theorem Proving in Higher Order Logics: 13th International Conference, pp.234-251, 2000.
DOI : 10.1007/3-540-44659-1_15

Y. Hida, X. S. Li, and D. H. Bailey, Algorithms for quad-double precision floating point arithmetic, Proceedings 15th IEEE Symposium on Computer Arithmetic. ARITH-15 2001, pp.155-162, 2001.
DOI : 10.1109/ARITH.2001.930115

N. J. Higham, Accuracy and Stability of Numerical Algorithms, SIAM, 2002.
DOI : 10.1137/1.9780898718027

W. Kahan, On the cost of floating-point computation without extra-precise arithmetic. World- Wide Web document, 2004.

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.
DOI : 10.1145/279232.279237
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.1679

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

V. Lefèvre, J. Muller, and A. Tisserand, Toward correctly rounded transcendentals, IEEE Transactions on Computers, vol.47, issue.11, pp.1235-1243, 1998.
DOI : 10.1109/12.736435

G. Melquiond, Floating-point arithmetic in the Coq system, Proceedings of the 8th Conference on Real Numbers and Computers, pp.93-102, 2008.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913

G. Melquiond, Proving Bounds on Real-Valued Functions with Computations, Proceedings of the 4th International Joint Conference on Automated Reasoning, pp.2-17, 2008.
DOI : 10.1007/978-3-540-71070-7_2
URL : https://hal.archives-ouvertes.fr/hal-00180138

G. Melquiond and S. Pion, Formally certified floating-point filters for homogeneous geometric predicates, Theoretical Informatics and Applications, pp.57-70, 2007.
DOI : 10.1051/ita:2007005
URL : https://hal.archives-ouvertes.fr/inria-00071232

D. Monniaux, The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, p.12, 2008.
DOI : 10.1145/1353445.1353446
URL : https://hal.archives-ouvertes.fr/hal-00128124

J. Muller, Elementary Functions, Algorithms and Implementation, Birkhäuser, 1997.
URL : https://hal.archives-ouvertes.fr/ensl-00000008

H. Mary, R. N. Payne, and . Hanek, Radian reduction for trigonometric functions, SIGNUM Newsletter, vol.18, pp.19-24, 1983.

D. M. Priest, Algorithms for arbitrary precision floating point arithmetic, [1991] Proceedings 10th IEEE Symposium on Computer Arithmetic, pp.132-144, 1991.
DOI : 10.1109/ARITH.1991.145549

J. R. Shewchuk, Adaptive Precision Floating-Point Arithmetic and Fast Robust Geometric Predicates, Discrete & Computational Geometry, vol.18, issue.3, pp.305-363, 1997.
DOI : 10.1007/PL00009321

P. H. Sterbenz, Floating point computation, 1974.

A. Ziv, Fast evaluation of elementary mathematical functions with correctly rounded last bit, ACM Transactions on Mathematical Software, vol.17, issue.3, pp.410-423, 1991.
DOI : 10.1145/114697.116813