[. Boehm, R. Cartwright, M. Riggle, and M. J. Donnell, Exact real arithmetic: a case study in higher order programming, Proceedings of the 1986 ACM conference on LISP and functional programming , LFP '86, pp.162-173, 1986.
DOI : 10.1145/319838.319860

S. Boldo and J. Filliâtre, Formal Verification of Floating-Point Programs, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.187-194, 2007.
DOI : 10.1109/ARITH.2007.20

URL : https://hal.archives-ouvertes.fr/hal-01174892

S. Boldo and C. Muñoz, A formalization of floating-point numbers in PVS, National Institute of Aerospace, 2006.

A. Bostan, Algorithmique efficace pour des opérations de base en Calcul formel, 2003.

L. Chen, A. Miné, and P. Cousot, A Sound Floating-Point Polyhedra Abstract Domain, Lecture Notes in Computer Science, vol.99, issue.2, pp.3-18, 2008.
DOI : 10.1007/3-540-45013-0_7

URL : https://hal.archives-ouvertes.fr/hal-00531567

C. Cohen, Construction of Real Algebraic Numbers in Coq, ITP -3rd International Conference on Interactive Theorem Proving -2012, 2012.
DOI : 10.1007/978-3-642-32347-8_6

URL : https://hal.archives-ouvertes.fr/hal-00671809

G. E. Collins, Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition, ACM SIGSAM Bulletin, vol.10, issue.1, pp.10-12, 1976.
DOI : 10.1145/1093390.1093393

P. Di, G. , and P. L. Lanzi, Lazy algorithms for exact real arithmetic, Electron. Notes Theor. Comput. Sci, vol.104, pp.113-128, 2004.

M. Daumas, G. Melquiond, and C. Muñoz, Guaranteed Proofs Using Interval Arithmetic, 17th IEEE Symposium on Computer Arithmetic (ARITH'05), pp.188-195, 2005.
DOI : 10.1109/ARITH.2005.25

URL : https://hal.archives-ouvertes.fr/hal-00164621

J. Harrison, Floating point verification in HOL, Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop, pp.186-199, 1985.
DOI : 10.1007/3-540-60275-5_65

R. Krebbers and B. Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, vol.9, issue.1, 2011.
DOI : 10.2168/LMCS-9(1:1)2013

M. Martel, Program transformation for numerical precision, Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation, PEPM '09, pp.101-110, 2009.
DOI : 10.1145/1480945.1480960

J. Maddalon, R. Butler, C. Muñoz, and G. Dowek, Mathematical basis for the safety analysis of conflict prevention algorithms, 2009.

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

P. Neron, A Formal Proof of Square Root and Division Elimination in Embedded Programs, Lecture Notes in Computer Science, vol.7679, pp.256-272, 2012.
DOI : 10.1007/978-3-642-35308-6_20

URL : https://hal.archives-ouvertes.fr/hal-00924367

P. Neron, Square Root and Division Elimination in PVS, Interactive Theorem Proving, pp.457-462, 2013.
DOI : 10.1007/978-3-642-39634-2_33

URL : https://hal.archives-ouvertes.fr/hal-00924359

A. Narkawicz, C. Muñoz, and G. Dowek, Formal verification of air traffic prevention bands algorithms, 2010.

A. Narkawicz, C. Muñoz, G. Russell, and O. Connor, Provably correct conflict prevention bands algorithms, Theorem Proving in Higher Order Logics, pp.1039-1057, 2012.
DOI : 10.1016/j.scico.2011.07.002

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.224.1835

A. K. Simpson, Lazy functional algorithms for exact real functionals, Mathematical Foundations of Computer Science, pp.456-464, 1998.
DOI : 10.1007/BFb0055795

A. Tarski, A Decision Method for Elementary Algebra and Geometry . Univ. of California Press, 1951.

J. Vuillemin, Exact real arithmetic with continued fractions, 1987.
DOI : 10.1145/62678.62681

URL : https://hal.archives-ouvertes.fr/inria-00075792

V. Weispfenning, Quantifier Elimination for Real Algebra -- the Quadratic Case and Beyond, Applicable Algebra in Engineering, Communication and Computing, vol.8, issue.2, pp.85-101, 1997.
DOI : 10.1007/s002000050055

E. Wiedmer, Computing with infinite objects, Theoretical Computer Science, vol.10, issue.2, pp.133-155, 1980.
DOI : 10.1016/0304-3975(80)90011-0

URL : http://doi.org/10.1016/0304-3975(80)90011-0