R. Bertot, F. Guilhot-and-l, and . Pottier, Visualizing Geometrical Statements with GeoView, User Interfaces for THeorem Provers (UITP'2003) of Electr. Notes Theor. Comput. Sci, pp.49-65, 2003.
DOI : 10.1016/j.entcs.2004.09.013

C. Cabri, 3D : logiciel de géométrie interactive 3D, 2006.

C. Development-team, . Inria, and . Lri, The Coq Proof Assistant Reference Manual, 2005.

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

]. F. Gui05 and . Guilhot, Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée, Revue des Sciences et Technologies de l'Information, TSI, pp.1113-1138, 2005.

]. R. Har02 and . Hartshorne, Geometry : Euclid and beyond, 2002.

]. D. Hil71 and . Hilbert, Les fondements de la géométrie, Éd. P. Rossier, Dunod, 1971.

D. Knuth, Axioms and Hulls. Number 606 in LNCS, 1991.

L. I. Meikle and J. D. Fleuriot, Formalizing Hilbert???s Grundlagen in Isabelle/Isar, TPHOLs'2003, pp.319-334, 2003.
DOI : 10.1007/10930755_21

A. Quaife, Automated Development of Fundamental Mathematical Theories, Éd. Kluwer, 1992.

J. and V. Plato, The axioms of constructive geometry, Annals of Pure and Applied Logic, vol.76, issue.2, pp.169-200, 1995.
DOI : 10.1016/0168-0072(95)00005-2