Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Boldo, Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms, Proceedings of the 3rd International Joint Conference on Automated Reasoning, pp.52-66, 2006.
DOI : 10.1007/11814771_6

S. Boldo and M. Daumas, Representable correcting terms for possibly underflowing floating point operations, 16th IEEE Symposium on Computer Arithmetic, 2003. Proceedings., pp.79-861207663, 2003.
DOI : 10.1109/ARITH.2003.1207663

S. Boldo, M. Daumas, C. Moreau-finot, and L. Théry, Computer validated proofs of a toolset for adaptable arithmetic, p.107025, 2001.
URL : https://hal.archives-ouvertes.fr/hal-00018530

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

M. Cornea, J. Harrison, C. Anderson, P. T. Tang, E. Schneider et al., A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format, IEEE Transactions on Computers, vol.58, issue.2, pp.148-162, 2009.
DOI : 10.1109/TC.2008.209

T. J. Dekker, A floating-point technique for extending the available precision, Numerische Mathematik, vol.5, issue.3, pp.224-242, 1971.
DOI : 10.1007/BF01397083

S. A. Figueroa, When is double rounding innocuous?, ACM SIGNUM Newsletter, vol.30, issue.3, 1995.
DOI : 10.1145/221332.221334

S. A. Figueroa, A rigorous framework for fully supporting the IEEE standard for floating-point arithmetic in high-level programming languages, 2000.

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

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

W. Kahan, Pracniques: further remarks on reducing truncation errors, Communications of the ACM, vol.8, issue.1, 1965.
DOI : 10.1145/363707.363723

W. Kahan, Lecture notes on the status of IEEE-754, 1996.

D. Knuth, The Art of Computer Programming, 1998.

O. Møller, Quasi double-precision in floating point addition, BIT, vol.7, issue.6, pp.37-50, 1965.
DOI : 10.1007/BF01975722

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

J. M. Muller, N. Brisebarre, F. De-dinechin, C. P. Jeannerod, V. Lefèvre et al., Handbook of Floating-Point Arithmetic, Birkhäuser Boston, 2010.
DOI : 10.1007/978-0-8176-4705-6
URL : https://hal.archives-ouvertes.fr/ensl-00379167

A. Neumaier, Rundungsfehleranalyse einiger Verfahren zur Summation endlicher Summen, ZAMM - Zeitschrift f??r Angewandte Mathematik und Mechanik, vol.50, issue.1, pp.39-51, 1974.
DOI : 10.1002/zamm.19740540106

Y. Nievergelt, Scalar fused multiply-add instructions produce floating-point matrix arithmetic provably accurate to the penultimate digit, ACM Transactions on Mathematical Software, vol.29, issue.1, pp.27-48, 2003.
DOI : 10.1145/641876.641878

T. Ogita, S. M. Rump, and S. Oishi, Accurate Sum and Dot Product, SIAM Journal on Scientific Computing, vol.26, issue.6, pp.1955-1988, 1137.
DOI : 10.1137/030601818
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.1547

M. Pichat, Correction d'une somme en arithmetique a virgule flottante, Numerische Mathematik, vol.19, issue.5, pp.400-406, 1972.
DOI : 10.1007/BF01404922

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

D. M. Priest, On properties of floating-point arithmetics: Numerical stability and the cost of accurate computations, 1992.

S. M. Rump, T. Ogita, and S. Oishi, -Fold Faithful and Rounding to Nearest, SIAM Journal on Scientific Computing, vol.31, issue.2, 2005.
DOI : 10.1137/07068816X
URL : https://hal.archives-ouvertes.fr/hal-00261004

S. M. Rump, T. Ogita, and S. Oishi, Accurate Floating-Point Summation Part I: Faithful Rounding, SIAM Journal on Scientific Computing, vol.31, issue.1, pp.189-224, 2008.
DOI : 10.1137/050645671

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.