Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry & Benjamin Werner (2011):
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses.
In: Jean-Pierre Jouannaud & Zhong Shao: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings,
Lecture Notes in Computer Science 7086.
Springer,
pp. 135–150,
doi:10.1007/978-3-642-25379-9_12.
Bruno Barras, Carst Tankink & Enrico Tassi (2015):
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface.
In: Christian Urban & Xingyuan Zhang: Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings,
Lecture Notes in Computer Science 9236.
Springer,
pp. 51–66,
doi:10.1007/978-3-319-22102-1_4.
Yves Bertot & Pierre Castéran (2004):
Interactive Theorem Proving and Program Development, \voidb@x Coq'Art : The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science, An EATCS Series.
Springer-Verlag,
Berlin/Heidelberg,
doi:10.1007/978-3-662-07964-5.
469 pages.
David Braun (2019):
Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective.
Université de Strasbourg.
Available at https://tel.archives-ouvertes.fr/tel-02512327.
David Braun, Nicolas Magaud & Pascal Schreck (2019):
Two Cryptomorphic Formalizations of Projective Incidence Geometry.
Annals of Mathematics and Artificial Intelligence 85(2–4),
pp. 193–212,
doi:10.1007/s10472-018-9604-z.
Available at https://hal.inria.fr/hal-01887000.
David Braun, Nicolas Magaud & Pascal Schreck (2021):
Two New Ways to Formally Prove Dandelin-Gallucci's Theorem.
In: Proceedings of the 2021 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC 2021, Saint Petersbourg (Virtual), Russia, July 18-23, 2021.
ACM,
pp. –,
doi:10.1145/3452143.3465550.
Coq development team (2021):
The Coq Proof Assistant Reference Manual, Version 8.13.2.
INRIA.
Available at http://coq.inria.fr.
David Delahaye (2000):
A Tactic Language for the System Coq.
In: Michel Parigot & Andrei Voronkov: Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings,
Lecture Notes in Computer Science 1955.
Springer,
pp. 85–95,
doi:10.1007/3-540-44404-1_7.
Laura Kovács & Andrei Voronkov (2013):
First-Order Theorem Proving and Vampire.
In: Natasha Sharygina & Helmut Veith: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings,
Lecture Notes in Computer Science 8044.
Springer,
pp. 1–35,
doi:10.1007/978-3-642-39799-8_1.
Nicolas Magaud, Julien Narboux & Pascal Schreck (2012):
A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem.
Computational Geometry: Theory and Applications 45(8),
pp. 406–424,
doi:10.1016/j.comgeo.2010.06.004.
Available at http://hal.inria.fr/inria-00432810/en.
Dominique Michelucci & Pascal Schreck (2006):
Incidence Constraints: a Combinatorial Approach.
Int. Journal of Computational Geometry and Applications 16(5-6),
pp. 443–460,
doi:10.1142/S0218195906002130.
Leonardo Mendonça de Moura & Nikolaj Bjørner (2008):
Z3: An Efficient SMT Solver.
In: Proceedings of TACAS 2008,
LNCS 4963.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
eptcs@eptcs.org