S. María-alpuente, J. Escobar, P. Meseguer, and . Ojeda, A Modular Equational Generalization Algorithm, Proceedings of Design and Application of Strategies/- Tactics in Higher Order Logics STRATA'03, pp.24-39, 2003.
DOI : 10.1016/S0747-7171(89)80012-4

A. Berry, X. Bouali, E. Fornari, E. Ledinot, R. Nassor et al., ESTEREL: a formal method applied to avionic software development, Science of Computer Programming, vol.36, issue.1, pp.5-25, 2000.
DOI : 10.1016/S0167-6423(99)00015-5
URL : https://hal.archives-ouvertes.fr/hal-00579632

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, PLDI, pp.196-207, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00128135

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

E. Peter, E. V. Bulychev, V. A. Kostylev, and . Zakharov, Antiunification algorithms and their applications in program analysis, Ershov Memorial Conference, pp.413-423, 2009.

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

F. Baader and T. Nipkow, Term rewriting and all that, p.51, 1998.

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

R. Bost, Nombres réels et transformation de programmes, p.115, 2012.

S. Boutin, Using reflection to build efficient and certified decision procedures, TACS'97, pp.515-529, 1997.
DOI : 10.1007/BFb0014565

C. W. Brown, An overview of QEPCAD B: a tool for real quantifier elimination and formula simplification, Journal of Japan Society for Symbolic and Algebraic Computation, vol.10, issue.1, pp.13-22, 2003.

F. Baader and W. Snyder, Unification theory, Handbook of Automated Reasoning, pp.445-532, 2001.

C. Barrett, C. Tinelli, and . Cvc3, CVC3, Lecture Notes in Computer Science, vol.4590, pp.298-302, 2007.
DOI : 10.1007/978-3-540-73368-3_34

C. Chaudhuri, S. Gulwani, and R. Lublinerman, The Coq development team. The Coq proof assistant reference manual Continuity and robustness of programs, Commun. ACM, vol.117, issue.8, pp.55107-115, 2012.

S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. Navid-pour, Proving programs robust, Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering, SIGSOFT/FSE '11, pp.102-112, 2011.
DOI : 10.1145/2025113.2025131

F. Cuoq, N. Kirchner, V. Kosmatov, J. Prevosto, B. Signoles et al., Frama-C, Proceedings of the 10th international conference on Software Engineering and Formal Methods, SEFM'12, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

A. Victor, P. S. Carreño, and . Miner, Specification of the IEEE-854 floatingpoint standard in HOL and PVS, 1995.

C. Cohen and A. Mahboubi, A Formal Quantifier Elimination for Algebraically Closed Fields, AISC/MKM/Calculemus, pp.189-203, 2010.
DOI : 10.1007/978-3-642-14128-7_17
URL : https://hal.archives-ouvertes.fr/inria-00464237

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

J. Paul and . Cohen, Decision procedures for real and p-adic fields, Communications on pure and applied mathematics, vol.22, issue.2, pp.131-151, 1969.

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

C. Cohen, Formalized algebraic numbers: construction and first-order theory, 2012.
URL : https://hal.archives-ouvertes.fr/pastel-00780446

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

D. Damian and O. Danvy, Syntactic accidents in program analysis: on the impact of the CPS transformation, Journal of Functional Programming, vol.13, issue.5, pp.867-904, 2003.
DOI : 10.1017/S0956796802004379

B. Dutertre and L. Mendonça-de-moura, A Fast Linear-Arithmetic Solver for DPLL(T), Lecture Notes in Computer Science, vol.4144, pp.81-94, 2006.
DOI : 10.1007/11817963_11

B. Dutertre and L. Mendonça-de-moura, The Yices SMT solver, p.130, 2006.

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

L. Mendonça-de-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

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

M. Daumas, L. Rideau, and L. Thery, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, 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

A. Dolzmann and T. Sturm, REDLOG, DS96b] Andreas Dolzmann and Thomas Sturm. Redlog User Manual, pp.2-9, 1996.
DOI : 10.1145/261320.261324

A. Goodloe, C. Muñoz, F. Kirchner, and L. Correnson, Verification of Numerical Programs: From Real Numbers to Floating Point Numbers, Proceedings of the 5th NASA Formal Methods Symposium, pp.441-446, 0131.
DOI : 10.1007/978-3-642-38088-4_31

[. Goubault, M. Martel, and S. Putot, Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter, Lecture Notes in Computer Science, vol.2305, issue.2, pp.209-212, 2002.
DOI : 10.1007/3-540-45927-8_15

D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-48, 1991.
DOI : 10.1145/103162.103163
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.7712

E. Goubault and S. Putot, Static Analysis of Finite Precision Computations, VMCAI, pp.232-247, 2011.
DOI : 10.1007/978-3-540-24738-8_18

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

J. Harrison, Metatheory and reflection in theorem proving: A survey and critique Available on the Web as http, 1995.

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

G. Huet, Resolution d'Equations dans les langages d'ordre 1, p.19, 1976.

M. Selmer, J. Johnson-]-temur-kutsia, M. Levy, and . Villaret, Generation of Permutations by Adjacent Transposition. Memorandum (Rand Corporation) Rand Corporation Anti-unification for unranked terms and hedges, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.114-219, 1963.

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

S. Lang, Algebraic Number Theory. Graduate Texts in Mathematics, p.32, 1994.

S. Lescuyer and S. Conchon, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, FroCoS, pp.287-303, 2009.
DOI : 10.1016/j.jal.2007.07.003

X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy et al., The OCaml system (release 4.00): Documentation and user's manual, Institut National de Recherche en Informatique et en Automatique, p.117, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00930213

J. Lassez, M. J. Maher, and K. Marriott, Unification revisited, Foundations of Deductive Databases and Logic Programming, pp.587-625, 1988.
DOI : 10.1007/3-540-19129-1_4

M. Martel, Semantics-Based Transformation of Arithmetic Expressions, SAS, pp.298-314, 2007.
DOI : 10.1007/978-3-540-74061-2_19

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. Muller, N. Brisebarre, C. Florent-de-dinechin, V. Jeannerod, G. Lefèvre et al., Handbook of Floating-Point Arithmetic, Birkhäuser Boston, vol.10, 2010.
DOI : 10.1007/978-0-8176-4705-6
URL : https://hal.archives-ouvertes.fr/ensl-00379167

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

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

A. Miné, Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, Lecture Notes in Computer Science, vol.2986, issue.2, pp.3-17, 2004.
DOI : 10.1007/978-3-540-24725-8_2

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

R. E. Moore, Methods and applications of interval analysis, SIAM studies in applied mathematics. SIAM, issue.2, 1995.
DOI : 10.1137/1.9781611970906

J. Napier, Mirifici logarithmorum canonis descriptio. Hart, Edimburgh, 1614. English translation by Edward Wright: A description of the admirable table of logarithmes, p.1616

P. Neron, A Formal Proof of Square Root and Division Elimination in Embedded Programs, Lecture Notes in Computer Science, vol.7679, issue.4, 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, Lecture Notes in Computer Science, vol.7998, issue.4, 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, Provably correct conflict prevention bands algorithms, Science of Computer Programming, vol.77, issue.10-11, pp.1039-1057, 2012.
DOI : 10.1016/j.scico.2011.07.002

[. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: a proof assistant for higher-order logic, p.117, 2002.
DOI : 10.1007/3-540-45949-9

E. L. Oberstar, Fixed-point representation & fractional math. Oberstar Consulting, revision, 2007.

O. Russell and . Connor, Certified exact transcendental real number computation in Coq, Theorem Proving in Higher Order Logics, pp.246-261, 2008.

C. Okasaki, Breadth-first numbering: lessons from a small exercise in algorithm design, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, ICFP '00, pp.131-136, 2000.

[. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, 11th International Conference on Automated Deduction 91 [OSW05] Cosmin Oancea, Clare So, and Stephen M. Watt. Generalization in Maple, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

[. Pfenning, Unification and anti-unification in the calculus of constructions, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.74-85, 1991.
DOI : 10.1109/LICS.1991.151632

D. Gordon, . Plotkinps83-]-h, R. Partsch, and . Steinbrüggen, A note on inductive generalization 19 [Pot89] Loïc Pottier Generalisation de termes en theorie equationnelle. Cas associatif-commutatif Program transformation systems, Machine Intelligence, pp.153-163, 1970.

C. John and . Reynolds, Transformational systems and the algebraic structure of atomic formulas. Machine intelligence, pp.135-151, 1970.

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

H. Rueß, Computational reflection in the calculus of constructions and its application to theorem proving, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97), p.119, 1997.

A. Seidenberg, A New Decision Method for Elementary Algebra, The Annals of Mathematics, vol.60, issue.2, pp.365-374, 1954.
DOI : 10.2307/1969640

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, p.13, 1951.

A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Journal of the London Mathematical Society, vol.42, issue.1, pp.230-265, 1936.

J. Vuillemin, Exact real arithmetic with continued fractions, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075792

V. Weispfenning, Quantifier elimination for real algebra---the cubic case, Proceedings of the international symposium on Symbolic and algebraic computation , ISSAC '94, pp.258-263, 1994.
DOI : 10.1145/190347.190425

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

M. Wildmoser and T. Nipkow, Certifying Machine Code Safety: Shallow Versus Deep Embedding, Lecture Notes in Computer Science, vol.3223, pp.305-320, 2004.
DOI : 10.1007/978-3-540-30142-4_22