J. Avigad, E. Dean, and J. Mumma, A FORMAL SYSTEM FOR EUCLID???S ELEMENTS, The Review of Symbolic Logic, vol.I???III, issue.04, pp.700-768, 2009.
DOI : 10.1007/s10817-007-9071-4

C. Dehlinger, J. F. Dufourd, and P. Schreck, Higher-Order Intuitionistic Formalization and Proofs in Hilbert???s Elementary Geometry, pp.306-324, 2000.
DOI : 10.1007/3-540-45410-1_17

L. C. Paulson, The Isabelle reference manual, 2006.

L. Meikle and J. Fleuriot, Formalizing Hilbert???s Grundlagen in Isabelle/Isar, LNCS, vol.2758, pp.319-334, 2003.
DOI : 10.1007/10930755_21

P. Scott and J. Fleuriot, An Investigation of Hilberts Implicit Reasoning through Proof Discovery in Idle-Time Automated Deduction in Geometry, Lecture Notes in Computer Science, vol.6877, pp.182200-182210, 2011.

A. Tarski and S. Givant, Abstract, Bulletin of Symbolic Logic, vol.I, issue.02, 1999.
DOI : 10.1090/S0002-9947-1902-1500592-8

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

A. Quaife, Automated development of Tarski's geometry, Journal of Automated Reasoning, vol.5, issue.1, pp.97-118, 1989.
DOI : 10.1007/BF00245024

H. N. Gupta, Contributions to the axiomatic foundations of geometry, 1965.

J. Narboux, Toward the use of a proof assistant to teach mathematics, The Seventh International Conference on Technology in Mathematics Teaching (ICTMT7), 2005.
URL : https://hal.archives-ouvertes.fr/inria-00495952

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

T. M. Pham, Description formelle de propriété géométriques, 2011.

D. Pichardie and Y. Bertot, Formalizing Convex Hull Algorithms, LNCS, vol.2152, pp.346-361, 2001.
DOI : 10.1007/3-540-44755-5_24

C. Brun, J. F. Dufourd, and N. Magaud, Designing and proving correct a convex hull algorithm with hypermaps in Coq, Computational Geometry, vol.45, issue.8, 2010.
DOI : 10.1016/j.comgeo.2010.06.006
URL : https://hal.archives-ouvertes.fr/hal-00955400

L. Meikle and J. Fleuriot, Mechanical theorem proving in computation geometry, pp.1-18, 2005.

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

J. Narboux, Formalisation et automatisation du raisonnement géométrique en Coq, 2006.

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

J. D. 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

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

T. M. Pham, Y. Bertot, and J. Narboux, A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry, The 11th International Conference on Computational Science and Its Applications, pp.368-383, 2011.
DOI : 10.1007/978-3-642-21898-9_32
URL : https://hal.archives-ouvertes.fr/inria-00584918

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

M. Sozeau and N. Oury, First-Class Type Classes, LNCS, vol.5170, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864