The following publications are possibly variants of this publication:
- A case study in formalizing projective geometry in Coq: Desargues theoremNicolas Magaud, Julien Narboux, Pascal Schreck. comgeo, 45(8):406-424, 2012. [doi]
- Formalizing Some "Small" Finite Models of Projective Geometry in CoqDavid Braun, Nicolas Magaud, Pascal Schreck. AISC 2018: 54-69 [doi]
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspectiveNicolas Magaud, Agathe Chollet, Laurent Fuchs. AMAI, 74(3-4):309-332, 2015. [doi]
- Formalization of the arithmetization of Euclidean plane geometry and applicationsPierre Boutry, Gabriel Braun, Julien Narboux. JSC, 90:149-168, 2019. [doi]
- A Coq-Based Library for Interactive and Automated Theorem Proving in Plane GeometryTuan-Minh Pham, Yves Bertot, Julien Narboux. iccsa 2011: 368-383 [doi]
- Two cryptomorphic formalizations of projective incidence geometryDavid Braun, Nicolas Magaud, Pascal Schreck. AMAI, 85(2-4):193-212, 2019. [doi]
- A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence GeometryDavid Braun, Nicolas Magaud, Pascal Schreck. JAR, 68(1):3, March 2024. [doi]