@inproceedings(SATCoq,
 author       = {Micha{\"{e}}l Armand and Germain Faure and Benjamin Gr{\'{e}}goire and Chantal Keller and Laurent Th{\'{e}}ry and Benjamin Werner},
 year         = {2011},
 title        = {A Modular Integration of {SAT/SMT} Solvers to Coq through Proof Witnesses},
 editor       = {Jean{-}Pierre Jouannaud and Zhong Shao},
 booktitle    = {Certified Programs and Proofs - First International Conference, {CPP} 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7086},
 publisher    = {Springer},
 pages        = {135--150},
 doi          = {10.1007/978-3-642-25379-9\_12},
)
@inproceedings(DBLP:conf/itp/BarrasTT15,
 author       = {Bruno Barras and Carst Tankink and Enrico Tassi},
 year         = {2015},
 title        = {Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface},
 editor       = {Christian Urban and Xingyuan Zhang},
 booktitle    = {Interactive Theorem Proving - 6th International Conference, {ITP} 2015, Nanjing, China, August 24-27, 2015, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9236},
 publisher    = {Springer},
 pages        = {51--66},
 doi          = {10.1007/978-3-319-22102-1\_4},
)
@book(BC04,
 author       = {Yves Bertot and Pierre Cast\'eran},
 year         = {2004},
 title        = {{I}nteractive {T}heorem {P}roving and {P}rogram {D}evelopment, \unhbox\voidb@x \hbox{{C}oq'{A}rt : {T}he} {C}alculus of {I}nductive {C}onstructions},
 series       = {Texts in Theoretical Computer Science, An EATCS Series},
 publisher    = {Springer-Verlag},
 address      = {Berlin/Heidelberg},
 doi          = {10.1007/978-3-662-07964-5},
 note         = {469 pages},
)
@phdthesis(Braun2019,
 author       = {David Braun},
 year         = {2019},
 title        = {{Approche combinatoire pour l'automatisation en Coq des preuves formelles en g{\'e}om{\'e}trie d'incidence projective}},
 school       = {{Universit{\'e} de Strasbourg}},
 url          = {https://tel.archives-ouvertes.fr/tel-02512327},
)
@article(BMS18a,
 author       = {David Braun and Nicolas Magaud and Pascal Schreck},
 year         = {2019},
 title        = {{Two Cryptomorphic Formalizations of Projective Incidence Geometry}},
 journal      = {{Annals of Mathematics and Artificial Intelligence}},
 volume       = {85},
 number       = {2--4},
 pages        = {193--212},
 doi          = {10.1007/s10472-018-9604-z},
 url          = {https://hal.inria.fr/hal-01887000},
)
@inproceedings(BMS21,
 author       = {David Braun and Nicolas Magaud and Pascal Schreck},
 year         = {2021},
 title        = {{Two New Ways to Formally Prove Dandelin-Gallucci's Theorem}},
 booktitle    = {Proceedings of the 2021 {ACM} on International Symposium on Symbolic and Algebraic Computation, {ISSAC} 2021, Saint Petersbourg (Virtual), Russia, July 18-23, 2021},
 publisher    = {{ACM}},
 pages        = {--},
 doi          = {10.1145/3452143.3465550},
)
@manual(coqmanual,
 author       = {{Coq development team}},
 year         = {2021},
 title        = {{The Coq Proof Assistant Reference Manual, Version 8.13.2}},
 organization = {INRIA},
 url          = {http://coq.inria.fr},
)
@inproceedings(DBLP:conf/lpar/Delahaye00,
 author       = {David Delahaye},
 year         = {2000},
 title        = {A Tactic Language for the System Coq},
 editor       = {Michel Parigot and Andrei Voronkov},
 booktitle    = {Logic for Programming and Automated Reasoning, 7th International Conference, {LPAR} 2000, Reunion Island, France, November 11-12, 2000, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1955},
 publisher    = {Springer},
 pages        = {85--95},
 doi          = {10.1007/3-540-44404-1\_7},
)
@inproceedings(vampire,
 author       = {Laura Kov{\'{a}}cs and Andrei Voronkov},
 year         = {2013},
 title        = {First-Order Theorem Proving and Vampire},
 editor       = {Natasha Sharygina and Helmut Veith},
 booktitle    = {Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {1--35},
 doi          = {10.1007/978-3-642-39799-8\_1},
)
@article(MNS12,
 author       = {Nicolas Magaud and Julien Narboux and Pascal Schreck},
 year         = {2012},
 title        = {{A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem}},
 journal      = {{Computational Geometry: Theory and Applications}},
 volume       = {45},
 number       = {8},
 pages        = {406--424},
 doi          = {10.1016/j.comgeo.2010.06.004},
 url          = {http://hal.inria.fr/inria-00432810/en},
)
@article(MS06,
 author       = {Dominique Michelucci and Pascal Schreck},
 year         = {2006},
 title        = {{Incidence Constraints: a Combinatorial Approach}},
 journal      = {{Int. Journal of Computational Geometry and Applications}},
 volume       = {16},
 number       = {5-6},
 pages        = {443--460},
 doi          = {10.1142/S0218195906002130},
)
@inproceedings(MouraB08,
 author       = {Leonardo Mendon{\c{c}}a de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{{Z3:} An Efficient {SMT} Solver}},
 booktitle    = {{Proceedings of TACAS 2008}},
 series       = {LNCS},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3_24},
)