T. The-ring, 12 1.3 Small scale reflection, p.13

.. Three, 39 4.9 A non structured interval membership goal 40 4.10 An interval membership goal, p.43

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, The Matita Interactive Theorem Prover, Proceedings of the 23rd international conference on Automated deduction, pp.64-69, 2011.
DOI : 10.1007/3-540-48256-3_12

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, Hints in Unification, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs '09, pp.84-98, 2009.
DOI : 10.1007/BFb0028402

J. Avigad, K. Donnelly, D. Gray, and P. Raff, A formally verified proof of the prime number theorem, ACM Transactions on Computational Logic, vol.9, issue.1, 2006.
DOI : 10.1145/1297658.1297660

G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Journal of Functional Programming, vol.13, issue.02, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-01124972

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

H. Bender and G. Glauberman, Local analysis for the Odd Order Theorem. Number 188 in London Mathematical Society Lecture Note Series, 1994.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development , Coq'Art: the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot, G. Gonthier, S. Ould-biha, and I. Pasca, Canonical Big Operators, Theorem Proving in Higher-Order Logics, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

Y. Bertot, F. Guilhot, and A. Mahboubi, A formal study of Bernstein coefficients and polynomials, Mathematical Structures in Computer Science, vol.21, issue.04, 2011.
DOI : 10.1017/S096012950600586X
URL : https://hal.archives-ouvertes.fr/inria-00503017

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Types for Proofs and Programs (TYPES 06), pp.48-62, 2006.
DOI : 10.1007/978-3-540-74464-1_4

. Sidi-ould and . Biha, Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton, Journées Francophones des Langages Applicatifs, 2008.

. Sidi-ould and . Biha, Finite groups representation theory with Coq, Mathematical Knowledge Management, 2009.

E. Bishop, Foundations of Constructive Analysis, 1967.

J. Bochnak, M. Coste, and M. Roy, Real Algebraic Geometry, Ergebnisse der Mathematik und ihrer Grenzgebiete, 1998.
DOI : 10.1007/978-3-662-03718-8

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

A. Bostan, F. Chyzak, M. Giusti, R. Lebreton, B. Salvy et al., Algorithmes efficaces en calcul formel, january 2012. En cours de rédaction, Notes de cours 2-22 du MPRI, 2010.

S. Boutin, Using reflection to build efficient and certified decision procedures, Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pp.515-529, 1007.
DOI : 10.1007/BFb0014565

A. Cauchy, Calcul des indices des fonctions, pp.176-229
DOI : 10.1017/CBO9780511702501.013

C. Chevalley and H. Cartan, Schémas normaux; morphismes; ensembles constructibles, Numdam, vol.8, pp.1-10

L. Chicli, L. Pottier, and C. Simpson, Mathematical Quotients and Quotient Types in Coq, Types for Proofs and Programs, number 2646 in LNCS, pp.95-107, 2003.
DOI : 10.1007/3-540-39185-1_6

C. Cohen, Types quotients en Coq, Actes des 21ème journées francophones des langages applicatifs, 2010.

C. Cohen, Construction des nombres algébriques en Coq, Proceedings of JFLA2012, 2012.

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 and T. Coquand, A constructive version of Laplace's proof on the existence of complex roots

C. Cohen and A. Mahboubi, A Formal Quantifier Elimination for Algebraically Closed Fields, Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, pp.189-203, 2010.
DOI : 10.1007/978-3-642-14128-7_17
URL : https://hal.archives-ouvertes.fr/inria-00464237

C. Cohen and A. Mahboubi, Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Logical Methods in Computer Science, vol.8, issue.1, pp.21-40, 2012.
URL : https://hal.archives-ouvertes.fr/inria-00593738

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.

G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition--preliminary report, ACM SIGSAM Bulletin, vol.8, issue.3, pp.80-90, 1974.
DOI : 10.1145/1086837.1086852

T. Coquand and G. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, 1986.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024

R. Cori and D. Lascar, Logique mathématique 1 -Calcul propositionnel ; algèbre de Boole ; calcul des prédicats réédition (avec corrections) de l'édition Masson, 1993.

P. Courtieu, Normalized Types, Proceedings of CSL2001, 2001.
DOI : 10.1007/3-540-44802-0_39

L. Cruz-filipe, A Constructive Formalization of the Fundamental Theorem of Calculus, Types for Proofs and Programs, pp.108-126, 2003.
DOI : 10.1007/3-540-39185-1_7

D. Delahaye, A Tactic Language for the System Coq, Logic for Programming and Automated Reasoning (LPAR), pp.85-95, 1955.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070

H. Derksen, The Fundamental Theorem of Algebra and Linear Algebra, The American Mathematical Monthly, vol.110, issue.7, pp.620-623, 2003.
DOI : 10.2307/3647746

M. Dénès, A. Mörtberg, and V. Siles, A Refinement-Based Approach to Computational Algebra in Coq, Interactive Theorem Proving, pp.83-98, 2012.
DOI : 10.1007/978-3-642-32347-8_7

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Theorem Proving in Higher Order Logics, TPHOLs 2009 proceedings, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11
URL : https://hal.archives-ouvertes.fr/inria-00368403

F. Garillot, Generic Proof Tools And Finite Group Theory, 2011.
URL : https://hal.archives-ouvertes.fr/pastel-00649586

C. Friedrich and G. , Another new proof of the theorem that every integral rational algebraic funcion of one variable can be resolved into real factors of the first or second degree, 1815.

H. Geuvers and M. Niqui, Constructive Reals in Coq: Axioms and Categoricity, Selected papers from the International Workshop on Types for Proofs and Programs, TYPES '00, pp.79-95, 2002.
DOI : 10.1007/3-540-45842-5_6

H. Geuvers, F. Wiedijk, and J. Zwanenburg, A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals, Lecture Notes in Computer Science, vol.2277, pp.96-111, 2000.
DOI : 10.1007/3-540-45842-5_7

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, Lecture Notes in Computer Science, vol.5081, p.333, 2007.
DOI : 10.1007/978-3-540-87827-8_28

G. Gonthier, Advances in the Formalization of the Odd Order Theorem, Lecture Notes in Computer Science, vol.6898, p.2, 2011.
DOI : 10.1007/978-3-642-22863-6_2

G. Gonthier, Point-Free, Set-Free Concrete Linear Algebra, Interactive Theorem Proving, ITP 2011 Proceedings, Lecture Notes in Computer Sciences, 2011.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-00805966

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

G. Gonthier, A. Mahboubi, and E. Tassi, A small scale reflection extension for the Coq system
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier and E. Tassi, A Language of Patterns for Subterm Selection, Interactive Theorem Proving, pp.361-376, 2012.
DOI : 10.1007/978-3-642-32347-8_25
URL : https://hal.archives-ouvertes.fr/hal-00652286

B. Gregoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, Theorem Proving in Higher Order Logics (TPHOLs 2005), pp.98-113, 2005.
DOI : 10.1007/11541868_7
URL : https://hal.archives-ouvertes.fr/hal-00819484

D. and Y. Grigor-'ev, Complexity of deciding Tarski algebra, Journal of Symbolic Computation, vol.5, issue.1-2, pp.65-108, 1988.
DOI : 10.1016/S0747-7171(88)80006-3

D. Yu, N. N. Grigor-'ev, and J. Vorobjov, Solving systems of polynomial inequalities in subexponential time, Journal of Symbolic Computation, vol.5, issue.12, pp.37-64, 1988.

J. Harrison, Formalizing an Analytic Proof of the Prime Number Theorem, Journal of Automated Reasoning, vol.104, issue.1:2, pp.243-261, 2009.
DOI : 10.1007/s10817-009-9145-6

M. Hedberg, A coherence theorem for martin-löf's type theory, Journal of Functional Programming, pp.4-8, 1998.

J. Heintz, M. Roy, and P. Solernó, Sur la complexit?? du principe de Tarski-Seidenberg, Bulletin de la Société mathématique de France, vol.118, issue.1, pp.101-126, 1990.
DOI : 10.24033/bsmf.2138

W. Hodges, A shorter model theory, 1997.

M. Hofmann, Extensional concepts in intensional type theory, 1995.

L. Hörmander, The analysis of linear partial differential operators, 1983.

P. Hudak, J. Peterson, and J. Fasel, Gentle introduction to haskell, version 98, 2000.

N. Julien and I. Pasca, Formal Verification of Exact Computations Using Newton???s Method, TPHOLs, pp.408-423, 2009.
DOI : 10.1007/3-540-36126-X_17

R. Krebbers and B. Spitters, Computer Certified Efficient Exact Reals in Coq, Conference on Intelligent Computer Mathematics, CICM 2011 Proceedings , Lecture Notes in Artifical Intelligence, 2011.
DOI : 10.1007/978-3-642-04027-6_12

S. Lang and . Algebra, Graduate texts in mathematics, 2002.

P. Laplace, Leçons de mathématiques données à l'École normale en 1795, Oeuvres complètes de Lapalace. Tome XIV, pp.10-177

H. Lombardi and C. Quitté, Algèbre commutative, Méthodes constructives, Calvage et Mounet, 2011.

R. Mines, F. Richman, and W. Ruitenburg, A course in constructive algebra, Universitext, 1979.
DOI : 10.1007/978-1-4419-8640-5

T. Nipkow, C. Ballarin, J. Avigad, and . Isabelle, HOL: Theory SetInterval

O. Russel and . Connor, Incompleteness & Completeness, Formalizing Logic and Analysis in Type Theory, 2009.

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

. Sidi-ould and . Biha, Composants mathématiques pour la théorie des groupes, 2010.

I. Pasca, Formal Proofs for Theoretical Properties of Newton's Method, 2010.

I. Pasca, Formally verified conditions for regularity of interval matrices, 17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, pp.219-233, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00464937

T. Peterfalvi, Character Theory for the Odd Order Theorem. Number 272 in London Mathematical Society Lecture Note Series, 2000.

J. Simon-peyton, The Haskell 98 language and libraries: The revised report, Journal of Functional Programming, vol.13, issue.1, pp.0-255, 2003.

F. Pfenning and C. Paulin-mohring, Inductively defined types in the Calculus of Constructions, Proceedings of Mathematical Foundations of Programmi ng Semantics, 1990.
DOI : 10.1007/BFb0040259

L. Pottier, Quotients dans le CCI, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00072584

J. Renegar, On the computational complexity and geometry of the firstorder theory of the reals. part i-iii, pp.255-352, 1992.

J. Robinson, Definability and decision problems in arithmetic, The Journal of Symbolic Logic, vol.4, issue.02, pp.98-114, 1949.
DOI : 10.1215/S0012-7094-47-01439-7

A. Saibi, Typing algorithm in type theory with inheritance, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.292-301, 1997.
DOI : 10.1145/263699.263742

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

M. Sozeau, A New Look at Generalized Rewriting in Type Theory, Journal of Formalized Reasoning, vol.2, issue.1, pp.41-62, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00628904

M. Sozeau and N. Oury, First-Class Type Classes, Theorem Proving in Higher Order Logics, TPHOLs 2008 proceedings, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

B. Spitters and E. Van-der-weegen, Type Classes for Mathematics in Type Theory. MSCS, special issue on 'Interactive theorem proving and the formalization of mathematics, pp.1-31, 2011.

P. Strub, Coq Modulo Theory, 19th EACSL Annual Conference on Computer Science Logic Computer Science Logic, CSL 2010, 19th Annual Conference of the EACSL, pp.529-543, 2010.
DOI : 10.1007/978-3-642-15205-4_40
URL : https://hal.archives-ouvertes.fr/inria-00497404

A. Tarski, . A-decision, E. Method, . Algebra, . Geometry et al., Republished as A Decision Method for Elementary Algebra and Geometry, 1948.

T. Braibant and D. Pous, Deciding Kleene Algebras in Coq, Logical Methods in Computer Science, vol.8, issue.1, p.2012
DOI : 10.2168/LMCS-8(1:16)2012
URL : https://hal.archives-ouvertes.fr/hal-00383070

B. Eelis-van-der-weegen, R. Spitters, and . Krebbers, Math classes