B. Barras, Sets in coq, coq in sets, Proceedings of the 1st Coq Workshop, 2009.

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

S. Berardi and S. Valentini, Krivine's intuitionistic proof of classical completeness (for countable languages), Annals of Pure and Applied Logic, vol.129, issue.1-3, pp.93-106, 2004.
DOI : 10.1016/j.apal.2004.01.002

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

B. Buchberger, Groebner Bases: Applications, The Concise Handbook of Algebra, pp.265-268, 2002.

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

G. Gonthier, F. Garillot, A. Mahboubi, and L. Rideau, Packaging mathematical structures, Lecture Notes in Computer Science, vol.5674, pp.327-342, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00368403

H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg, A Constructive Algebraic Hierarchy in Coq, Journal of Symbolic Computation, vol.34, issue.4, pp.271-286, 2002.
DOI : 10.1006/jsco.2002.0552

J. Harrison, Complex quantifier elimination in HOL Division of Informatics, TPHOLs 2001: Supplemental Proceedings Published as Informatics Report Series EDI-INF-RR-0046. Available on the Web, pp.159-174, 2001.

W. Hodges, A shorter model theory, 1997.

K. Gödel, ¨ Uber die Vollständigkeit des Logikkalküls, 1929.

T. Nipkow, Linear quantifier elimination, Automated Reasoning, pp.18-33, 2008.

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

L. Pottier, Connecting gröbner bases programs with coq to do proofs in algebra, geometry and arithmetics, LPAR Workshops CEUR Workshop Proceedings. CEUR-WS.org, 2008.

T. Ridge and J. Margetson, A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic, Lecture Notes in Computer Science, vol.3603, pp.294-309, 2005.
DOI : 10.1007/11541868_19

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

C. T. Simpson, Formalized proof, computation, and the construction problem in algebraic geometry, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00003021

A. Tarski, A Decision Method for Elementary Algebra and Geometry
DOI : 10.1007/978-3-7091-9459-1_3

. S. Manuscript, C. Monica, and . Corp, Republished as A Decision Method for Elementary Algebra and Geometry, 1948.