J. Avigad, E. Dean, and J. Mumma, A formal system for euclids elements. The Review of Symbolic Logic, pp.700-768, 2009.

G. Barthe, J. Forest, D. Pichardie, and V. Rusu, Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant, Functional and Logic Programming (FLOPS'06), 2006.
DOI : 10.1007/11737414_9
URL : https://hal.archives-ouvertes.fr/inria-00564237

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions . Texts in Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Boutin, Using reflection to build efficient and certified decision procedures, Theoretical Aspects of Computer Software, p.515529, 1997.
DOI : 10.1007/BFb0014565

P. Boutry, J. Narboux, and P. Schreck, Parallel postulates and decidability of intersection of lines: a mechanized study within Tarski's system of geometry. submitted URL https, 2015.

G. Braun and J. Narboux, From Tarski to Hilbert, URL https, pp.89-109, 2012.
DOI : 10.1007/978-3-642-40672-0_7
URL : https://hal.archives-ouvertes.fr/hal-00727117

G. Braun and J. Narboux, A synthetic proof of Pappus' theorem in Tarski's geometry URL https, Journal of Automated Reasoning, 2015.

S. Chou, Mechanical Geometry Theorem Proving, 1988.
DOI : 10.1007/978-94-009-4037-6

S. Chou, X. Gao, and J. Zhang, Machine Proofs in Geometry, World Scientific, vol.6, 1994.
DOI : 10.1142/2196

J. Duprat, Fondements de géométrie euclidienne URL https, 2010.

L. Fuchs and L. Théry, A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry, Automated Deduction in Geometry, ADG 2010 URL https, pp.51-62, 2010.
DOI : 10.1007/978-3-7091-4368-1
URL : https://hal.archives-ouvertes.fr/hal-00657901

J. Genevaux, J. Narboux, and P. Schreck, Formalization of Wu???s Simple Method in Coq, CPP 2011 First International Conference on Certified Programs and Proofs, pp.71-86, 2011.
DOI : 10.1007/978-3-642-21046-4_10

B. Grégoire, L. Pottier, and L. Théry, Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving Automated Deduction in Geometry, Lecture Notes in Computer Science, vol.6301, pp.4259978-4259981, 2011.

F. Guilhot, Formalisation en Coq et visualisation d'un cours de g??om??trie pour le lyc??e, Techniques et sciences informatiques, vol.24, issue.9, pp.1113-1138, 2005.
DOI : 10.3166/tsi.24.1113-1138

P. Janicic, J. Narboux, and P. Quaresma, The Area Method, Journal of Automated Reasoning, vol.13, issue.3, pp.489-532, 2012.
DOI : 10.1007/s10817-010-9209-7
URL : https://hal.archives-ouvertes.fr/hal-00426563

S. Lescuyer, First-class containers in coq URL http://studia.complexica.net/ index.php?option=com_content&view=article&id=187% 3Afirst-class-containers-in-coq, Stud. Inform. Univ, vol.9, issue.1, pp.87-12787, 2011.

H. Li, Automated Geometric Theorem Proving, Clifford Bracket Algebra and Clifford Expansions Advances in Analysis and Geometry, Trends in Mathematics Birkhuser Basel, pp.345363-978, 2004.

N. Magaud, J. Narboux, and P. Schreck, Formalizing Desargues' theorem in Coq using ranks, Proceedings of the 2009 ACM symposium on Applied Computing, SAC '09, pp.1110-1115, 2009.
DOI : 10.1145/1529282.1529527
URL : https://hal.archives-ouvertes.fr/inria-00335719

N. Magaud, J. Narboux, and P. Schreck, A case study in formalizing projective geometry in Coq: Desargues theorem, URL https, pp.406-424, 2012.
DOI : 10.1016/j.comgeo.2010.06.004
URL : https://hal.archives-ouvertes.fr/inria-00432810

J. Narboux, A Decision Procedure for Geometry in Coq, Theorem Proving in Higher Order Logics URL https, pp.225-240, 2004.
DOI : 10.1007/978-3-540-30142-4_17
URL : https://hal.archives-ouvertes.fr/inria-00001035

J. Narboux, Mechanical Theorem Proving in Tarski's geometry Automated Deduction in Geometry, pp.139-156, 2006.

M. Pasch, Vorlesungen ber neuere Geometrie, 1976.

L. Pottier, Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics, Knowledge Exchange: Automated Provers and Proof Assistants, CEUR Workshop Proceedings, p.418, 2008.

W. Schwabhauser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie, 1983.
DOI : 10.1007/978-3-642-69418-9

P. Scott, Mechanising Hilberts foundations of geometry in Isabelle, 2008.

P. Scott, J. Fleuriot, J. Jeuring, J. Campbell, J. Carette et al., A Combinator Language for Theorem Discovery, Intelligent Computer Mathematics Lecture Notes in Computer Science, vol.7362, pp.371385978-371385981
DOI : 10.1007/978-3-642-31374-5_25

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

A. Tarski, What is Elementary Geometry? The axiomatic Method, with special reference to Geometry and Physics, pp.16-29, 1959.

L. Théry, A Machine-Checked Implementation of Buchberger's Algorithm, Journal of Automated Reasoning, vol.26, issue.2, p.107137, 2001.

W. Wu, ON THE DECISION PROBLEM AND THE MECHANIZATION OF THEOREM-PROVING IN ELEMENTARY GEOMETRY, Scientia Sinica, vol.21, pp.157-179, 1978.
DOI : 10.1142/9789812791085_0008