S. Basu, R. Pollack, and M. Roy, Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics), 2006.

C. W. Brown, QEPCAD B, ACM SIGSAM Bulletin, vol.37, issue.4, pp.97-108, 2003.
DOI : 10.1145/968708.968710

F. Caruso, The SARAG Library: Some Algorithms in Real Algebraic Geometry, pp.122-131, 2006.
DOI : 10.1007/11832225_11

B. F. Caviness and J. R. Johnson, Quantifier Elimination and Cylindrical Algebraic Decomposition, 2012.
DOI : 10.1007/978-3-7091-9459-1

C. Cohen, Finmap Library. https://github, p.7, 2017.

C. Cohen, Construction of Real Algebraic Numbers in Coq, 2012.
DOI : 10.1007/978-3-642-32347-8_6
URL : https://hal.archives-ouvertes.fr/hal-00671809

C. Cohen, Pragmatic Quotient Types in Coq, Interactive Theorem Proving -4th International Conference Proceedings. 213?228, pp.978-981, 2013.
DOI : 10.1007/978-3-642-39634-2_17

C. Cohen and A. Mahboubi, A Formal Quantifier Elimination for Algebraically Closed Fields, Intelligent Computer Mathematics , 10th International Conference 17th Symposium, Calculemus 2010, and 9th International Conference Proceedings. 189?203, pp.978-981, 2010.
DOI : 10.1007/978-3-642-14128-7_17
URL : https://hal.archives-ouvertes.fr/inria-00464237

M. Eberl, A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pp.75-83, 2015.
DOI : 10.1145/362575.362577

L. Gonzalez-vega, H. Lombardi, and L. Mahé, Virtual roots of real polynomials, Journal of Pure and Applied Algebra, vol.124, issue.1-3, pp.147-166, 1998.
DOI : 10.1016/S0022-4049(96)00102-8
URL : https://doi.org/10.1016/s0022-4049(96)00102-8

J. Harrison, Verifying the accuracy of polynomial approximations in HOL, Theorem Proving in Higher Order Logics: 10th International Conference, pp.137-152, 1997.
DOI : 10.1007/BFb0028391

J. Harrison, Formalizing basic first order model theory, Theorem Proving in Higher Order Logics: 11th International Conference, pp.153-170, 1998.
DOI : 10.1007/BFb0055135
URL : http://www.cl.cam.ac.uk/~jrh13/papers/model.ps.gz

J. Harrison, Handbook of Practical Logic and Automated Reasoning, 2009.
DOI : 10.1017/CBO9780511576430

J. Harrison, Theorem Proving with the Real Numbers, 2011.
DOI : 10.1007/978-1-4471-1591-5
URL : ftp://ftp.cl.cam.ac.uk/papers/reports/TR408-jrh-Theorem-Proving-with-the-Real-Numbers.ps.gz

S. Lescuyer, Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00713668

W. Li and L. C. Paulson, A Formal Proof of Cauchy???s Residue Theorem, pp.235-251978, 2016.
DOI : 10.1007/978-3-642-59273-7

A. Mahboubi, lstcoq.sty file which defines a Coq -SSReflect style for listings in Latex, pp.8-10, 2017.

A. Mahboubi, Contributions à la certification des calculs dans R : théorie, preuves, programmation. (Contributions to the certification of computations in R : theory, proofs, implementation). Ph.D. Dissertation, 2006.

A. Mahboubi, Implementing the cylindrical algebraic decomposition within the Coq system, Mathematical Structures in Computer Science, vol.17, issue.01, pp.99-127, 2007.
DOI : 10.1017/S096012950600586X
URL : https://hal.archives-ouvertes.fr/hal-00819489

A. Mahboubi and E. Tassi, Mathematical Components. https://math-comp.github, p.6, 2017.

A. Narkawicz, C. Muñoz, and A. Dutle, Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm???s and Tarski???s Theorems, Journal of Automated Reasoning, vol.51, issue.2, pp.285-326, 2015.
DOI : 10.1007/978-3-7643-7990-2_29

C. Paulin-mohring, Introduction to the Coq Proof- Assistant for Practical Software Verification In Tools for Practical Software Verification, LASER, pp.45-95, 2011.

A. Tarski, A Decision Method for Elementary Algebra and Geometry, Bull. Amer. Math. Soc, p.59, 1951.
DOI : 10.1007/978-3-7091-9459-1_3

C. Lawrence, . Paulson-wenda, G. O. Li, and . Passmore, A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle, 2015.

. Wikipedia, CAD. https://en.wikipedia.org/wiki/Cylindrical_ algebraic_decomposition, p.11, 2017.