P. Boutry, G. Braun, and J. Narboux, From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry, The 7th International Symposium on Symbolic Computation in Software EasyChair Proceedings in Computing, p.15, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01282550

M. Beeson, Proof and Computation in Geometry, Springer Lecture Notes in Artificial Intelligence, vol.7993, pp.1-30, 2012.
DOI : 10.1007/978-3-642-40672-0_1

M. Beeson, A constructive version of Tarski's geometry, Annals of Pure and Applied Logic, vol.166, issue.11, pp.1199-1273, 1974.
DOI : 10.1016/j.apal.2015.07.006

M. Bezem and D. Hendriks, On the Mechanization of the Proof of Hessenberg???s Theorem in Coherent Logic, Journal of Automated Reasoning, vol.19, issue.1, pp.61-85, 2008.
DOI : 10.1007/s10817-007-9086-x

G. Braun and J. Narboux, From Tarski to Hilbert Post-proceedings of Automated Deduction in Geometry 2012, Tetsuo Ida and Jacques Fleuriot, pp.89-109, 2012.

P. Boutry, J. Narboux, and P. Schreck, A reflexive tactic for automated generation of proofs of incidence to an affine variety, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01216750

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, 2015.

P. Boutry, J. Narboux, P. Schreck, and G. Braun, A short note about case distinctions in Tarski's geometry, Automated Deduction in Geometry 2014, Proceedings of ADG 2014, pp.1-15, 2014.

P. Boutry, J. Narboux, P. Schreck, and G. Braun, Using small scale automation to improve both accessibility and readability of formal proofs in geometry, Automated Deduction in Geometry 2014, Proceedings of ADG 2014, pp.1-19, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00989781

P. Castéran, +. Coq, J. In, J. Dehlinger, P. Dufourd et al., Higher-Order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry, Automated Deduction in Geometry, pp.1-15, 2000.

B. Grégoire, L. Pottier, and L. Théry, Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving, Postproceedings of Automated Deduction in Geometry number 6701 in Lecture Notes in Artificial Intelligence, 2008.
DOI : 10.1007/978-3-642-21046-4_3

D. Hilbert, Foundations of Geometry (Grundlagen der Geometrie) Open Court Second English edition, translated from the tenth German edition by Leo Unger. Original publication date, 1899 The Area Method : a Recapitulation, JNQ12] Predrag Janicic, Julien Narboux, and Pedro Quaresma, pp.489-532, 1960.

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

J. Narboux, Mechanical Theorem Proving in Tarski's geometry Post-proceedings of Automated Deduction in Geometry Classical configurations in affine planes, LNCS Journal of formalized mathematics, vol.4869, issue.2, pp.139-156, 1990.

M. Pasch, M. Vorlesungen-Über-neuere-geometrie, N. Sozeau, and . Oury, First-Class Type Classes, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie, pp.278-293, 1976.