M. Beeson, Constructive geometry and the parallel postulate. Bulletin of Symbolic Logic, accepted pending revisions, 2015.

M. Beeson, A constructive version of Tarski's geometry. Annals of Pure and Applied Logic, pp.1199-1273, 2015.

G. David and B. , A set of postulates for plane geometry (based on scale and protractors), Annals of Mathematics, vol.33, 1932.

D. Braun and N. Magaud, Des preuves formelles en Coq du théorème de Thalès pour les cercles, Vingt-sixièmes Journées Francophones des Langages Applicatifs, 2015.

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

]. M. Deh00 and . Dehn, Die Legendre'schen Sätze über die Winkelsumme im Dreieck, Mathematische Annalen, vol.53, issue.3, pp.404-439, 1900.

J. Duprat, Une axiomatique de la géométrie plane en Coq, JFLA (Journées Francophones des Langages Applicatifs), pp.123-136, 2008.

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

M. J. Greenberg, Euclidean and Non-Euclidean Geometries -Development and History, 1993.

M. J. Greenberg, Old and New Results in the Foundations of Elementary Plane Euclidean and Non-Euclidean Geometries, The American Mathematical Monthly, vol.117, issue.3, pp.198-219, 2010.
DOI : 10.4169/000298910x480063

[. Gupta, Contributions to the axiomatic foundations of geometry, 1965.

]. G. Klu63, Conatuum praecipuorum theoriam parallelarum demonstrandi recensio German translation available, 1763.

[. Makarios, A Mechanical Verification of the Independence of Tarski's Euclidean Axiom, 2012.

]. G. Mar98 and . Martin, The Foundations of Geometry and the Non-Euclidean Plane, Undergraduate Texts in Mathematics, 1998.

F. Mari? and D. Petrovi?, Formalizing complex plane geometry, Annals of Mathematics and Artificial Intelligence, vol.13, issue.2, pp.1-38, 2014.
DOI : 10.1007/s10472-014-9436-4

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

[. Petrovi? and F. Mari?, Formalizing analytic geometries, Proceedings of Automated Deduction in Geometry, 2012.

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

A. Tarski and S. Givant, Tarski's system of geometry. The bulletin of Symbolic Logic, 1999.