Y. Bertot, F. Guilhot, and L. Pottier, Visualizing Geometrical Statements with GeoView, Electronic Notes in Theoretical Computer Science, vol.103, pp.49-65, 2003.
DOI : 10.1016/j.entcs.2004.09.013
URL : http://doi.org/10.1016/j.entcs.2004.09.013

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

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

D. Hilbert, Les fondements de la géométrie, edition critique avec introduction et compléments préparée par Paul Rossier, 1971.

P. Janici´cjanici´c, Geometry Constructions Language, Journal of Automated Reasoning, vol.174, issue.2, pp.3-24, 2010.
DOI : 10.1007/s10817-009-9135-8

P. Janicic, J. Narboux, and P. Quaresma, The Area Method : a Recapitulation, Journal of Automated Reasoning, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00426563

L. Meikle and J. Fleuriot, Formalizing Hilbert???s Grundlagen in Isabelle/Isar, Theorem Proving in Higher Order Logics, pp.319-334, 2003.
DOI : 10.1007/10930755_21

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

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

J. Narboux, A Graphical User Interface for Formal Proofs in Geometry, Journal of Automated Reasoning, vol.17, issue.2, pp.161-180, 2007.
DOI : 10.1007/s10817-007-9071-4
URL : https://hal.archives-ouvertes.fr/inria-00118903

J. Narboux, Mechanical Theorem Proving in Tarski???s Geometry, ADG'06. LNAI, pp.139-156, 2007.
DOI : 10.1007/978-3-540-77356-6_9

T. M. Pham and Y. Bertot, A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs, Electronic Notes in Theoretical Computer Science, vol.285, p.10, 2010.
DOI : 10.1016/j.entcs.2012.06.005
URL : https://hal.archives-ouvertes.fr/inria-00585400

P. Scott and J. Fleuriot, Idle time discovery in geometry theorem proving, Proceedings of ADG, p.10, 2010.

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