@incollection{harrison05,
  title={A {HOL} theory of {Euclidean} space},
  author={Harrison, John},
  booktitle={Theorem proving in higher order logics},
  pages={114--129},
  year={2005},
  publisher={Springer}
}

@incollection{wlog,
  title={Without loss of generality},
  author={Harrison, John},
  booktitle={Theorem Proving in Higher Order Logics},
  pages={43--59},
  year={2009},
  publisher={Springer}
}

@book{schwerdtfeger,
  title={Geometry of complex numbers: circle geometry, {Moebius} transformation, non-euclidean geometry},
  author={Schwerdtfeger, Hans},
  year={1979},
  publisher={Courier Corporation}
}

@book{needham,
  title={Visual complex analysis},
  author={Needham, Tristan},
  year={1998},
  publisher={Oxford University Press}
}

@book{hilbert,
  title={Grundlagen der geometrie},
  author={Hilbert, David},
  year={2013},
  publisher={Springer-Verlag}
}

@incollection{hilbert-coq,
  title={Higher-order intuitionistic formalization and proofs in {Hilbert’s} elementary geometry},
  author={Dehlinger, Christophe and Dufourd, Jean-Fran{\c{c}}ois and Schreck, Pascal},
  booktitle={Automated Deduction in Geometry},
  pages={306--323},
  year={2001},
  publisher={Springer}
}

@incollection{hilbert-isabelle,
  title={Formalizing {Hilbert’s} {Grundlagen} in {Isabelle/Isar}},
  author={Meikle, Laura I and Fleuriot, Jacques D},
  booktitle={Theorem proving in higher order logics},
  pages={319--334},
  year={2003},
  publisher={Springer}
}

@article{hilbert-scott,
  title={Mechanising {Hilbert’s} foundations of geometry in {Isabelle}},
  author={Scott, Phil},
  journal={Master's thesis, University of Edinburgh},
  year={2008},
  publisher={Citeseer}
}

@book{tarski,
  author =   {Wolfram Schwabhäuser and Wanda Szmielew and Alfred Tarski},
  title =    {{Metamathematische Methoden in der Geometrie}},
  publisher =    {Springer-Verlag},
  year =   {1983},
  address =    {Berlin}
}

@incollection{narboux-tarski,
  title={Mechanical theorem proving in {Tarski’s} geometry},
  author={Narboux, Julien},
  booktitle={Automated Deduction in Geometry},
  pages={139--156},
  year={2007},
  publisher={Springer}
}

@article{von-plato-formalization,
  title={Constructive geometry according to {Jan} von {Plato}},
  author={Kahn, Gilles},
  journal={Coq contribution. Coq},
  volume={5},
  pages={10},
  year={1995}
}

@article{vonPlato,
  title={The axioms of constructive geometry},
  author={von Plato, Jan},
  journal={Annals of pure and applied logic},
  volume={76},
  number={2},
  pages={169--200},
  year={1995},
  publisher={Elsevier}
}

@article{guilhot,
  title={Formalisation en {Coq} et visualisation d'un cours de g{\'e}om{\'e}trie pour le lyc{\'e}e.},
  author={Guilhot, Fr{\'e}d{\'e}rique},
  journal={Technique et Science informatiques},
  volume={24},
  number={9},
  pages={1113--1138},
  year={2005}
}

@article{duprat2008,
  title={Une axiomatique de la g{\'e}om{\'e}trie plane en {Coq}},
  author={Duprat, Jean},
  journal={Actes des JFLA},
  pages={123--136},
  year={2008}
}

@inproceedings{petrovic2012formalizing,
  title={Formalizing analytic geometries},
  author={Petrovic, Danijela and Maric, Filip},
  booktitle={This volume contains the papers presented at ADG 2012: The 9th International Workshop on Automated Deduction in Geometry, held on September 17--19, 2012 at the University of Edinburgh. The submissions were each reviewed by at least 3 program committee mem-bers, and the committee decided to accept 15 papers for the workshop. The},
  pages={107},
  year={2012}
}

