D. H. Bailey, R. Krasny, and R. Pelz, Multiple precision, multiple processor vortex sheet roll-up computation, Proceedings of the Sixth SIAM Conference on Parallel Processing for Scientific Computing, pp.52-56, 1993.

G. Barrett, Formal methods applied to a floating-point number system, IEEE Transactions on Software Engineering, vol.15, issue.5, pp.611-621, 1989.
DOI : 10.1109/32.24710

G. Bohlender, W. Walter, P. Kornerup, and D. W. Matula, Semantics for exact floating point operations, [1991] Proceedings 10th IEEE Symposium on Computer Arithmetic, pp.22-26, 1991.
DOI : 10.1109/ARITH.1991.145529

C. Burnikel, R. Fleischer, K. Mehlhorn, and S. Schirra, Efficient exact geometric computation made easy, Proceedings of the fifteenth annual symposium on Computational geometry , SCG '99, pp.341-350, 1999.
DOI : 10.1145/304893.304988
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.865

W. J. Cody, Static and dynamic numerical characteristics of floating point arithmetic, IEEE Transactions on Computers, vol.22, issue.6, pp.598-601, 1973.

W. J. Cody and R. Karpinski, A Proposed Radix- and Word-length-independent Standard for Floating-point Arithmetic, IEEE Micro, vol.4, issue.4, pp.86-100, 1984.
DOI : 10.1109/MM.1984.291224

M. Daumas, Multiplications of floating point expansions, Proceedings 14th IEEE Symposium on Computer Arithmetic (Cat. No.99CB36336), pp.250-257, 1999.
DOI : 10.1109/ARITH.1999.762851

M. Daumas and C. Finot, Division of Floating-Point Expansions with an application to the computation of a determinant, Journal of Universal Computer Science, vol.5, issue.6, pp.323-338, 1999.

M. Daumas and P. Langlois, Additive symmetric: the non-negative case, Theoretical Computer Science, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00072516

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

J. Filliâtre, Proof of Imperative Programs in Type Theory, International Workshop, TYPES '98, Kloster Irsee number 1657 in LNCS, 1998.
DOI : 10.1007/3-540-48167-2_6

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

J. C. Michael, T. F. Gordon, and . Melham, Introduction to HOL : a theorem proving environment for higher-order logic, 1993.

T. Granlund, The GNU multiple precision arithmetic library, 2000.

J. Harrison, A Machine-Checked Theory of Floating Point Arithmetic, Bertot et al. [3], pp.113-130
DOI : 10.1007/3-540-48256-3_9

N. J. Higham, Accuracy and stability of numerical algorithms, SIAM, 1996.
DOI : 10.1137/1.9780898718027

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq Proof Assistant: A Tutorial: Version 6.1, 1997.
URL : https://hal.archives-ouvertes.fr/inria-00069967

V. Karamcheti, C. Li, I. Pechtchanski, and C. Yap, A core library for robust numeric and geometric computation, Proceedings of the fifteenth annual symposium on Computational geometry , SCG '99, pp.351-359, 1999.
DOI : 10.1145/304893.304989

R. Karpinski, PARANOIA: a floating-point benchmark, Byte, vol.10, issue.2, pp.223-235, 1985.

M. Kaufmann, P. Manolios, and J. Strother-moore, Computer-Aided Reasoning: An Approach. advances in formal methods, 2000.

E. Donald and . Knuth, The art of computer programming: Seminumerical Algorithms, 1973.

A. Michael and . Malcolm, Algorithms to reveal properties of floating-Point Arithmetic, Communications of the ACM, vol.15, issue.11, pp.949-951, 1972.

M. Mayero, The Three Gap Theorem: Specification and Proof in Coq, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00072808

P. S. Miner, Defining the IEEE-854 floating-point standard in pvs, 1995.

O. Møller, Note on quasi double-precision, BIT, vol.8, issue.5, pp.251-255, 1965.
DOI : 10.1007/BF01937505

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

D. M. Priest, On Properties of Floating Point Arithmetics: Numerical Stability and the Cost of Accurate, 1993.

F. John, D. E. Reiser, and . Knuth, Evading the drift in floating point addition, Information Processing Letter, vol.3, issue.3, pp.84-87, 1975.

J. M. Rushby, N. Shankar, and M. Srivas, PVS: Combining specification, proof checking, and model checking, CAV '96, 1996.

M. David and . Russinoff, A Mechanically Checked Proof of IEEE Compliance of the AMD K5 Floating-Point Square Root Microcode. Formal Methods in System Design, pp.75-125, 1999.

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

M. J. Spivey, Understanding Z: A Specification Language and its Formal Semantics . Cambridge Tracts in Theoretical Computer Science, 1988.

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

D. Stevenson, An american national standard: IEEE standard for binary floating point arithmetic, ACM SIGPLAN Notices, vol.22, issue.2, pp.9-25, 1987.

M. Wenzel, Isar ??? A Generic Interpretative Approach to Readable Formal Proof Documents, Bertot et al. [3], pp.167-184
DOI : 10.1007/3-540-48256-3_12