References

  1. 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.
  2. Anton Betten (2016): The packings of PG(3, 3). Designs, Codes and Cryptography 79(3), pp. 583–595, doi:10.1007/s10623-015-0074-6.
  3. David Braun, Nicolas Magaud & Pascal Schreck (2018): Formalizing Some "Small" Finite Models of Projective Geometry in Coq. In: Jacques Fleuriot, Dongming Wang & Jacques Calmet: Proceedings of Artificial Intelligence and Symbolic Computation 2018 (AISC'2018), LNAI 11110, pp. 54–69, doi:10.1007/978-3-319-99957-9_4. Available at https://hal.inria.fr/hal-01835493.
  4. R.H Bruck & R.C Bose (1964): The construction of translation planes from projective spaces. Journal of Algebra 1(1), pp. 85–102, doi:10.1016/0021-8693(64)90010-9.
  5. Francis Buekenhout (1995): Handbook of Incidence Geometry. North Holland.
  6. F. N. Cole (1922): Kirkman parades. Bull. Amer. Math. Soc. 28(9), pp. 435–437, doi:10.1090/S0002-9904-1922-03599-9. Available at https://projecteuclid.org:443/euclid.bams/1183485271.
  7. Coq development team (2021): The Coq Proof Assistant Reference Manual, Version 8.13.2. INRIA. Available at http://coq.inria.fr.
  8. Harold Scott Macdonald Coxeter (2003): Projective Geometry. Springer Science & Business Media.
  9. Georges Gonthier & Assia Mahboubi (2008): A Small Scale Reflection Extension for the Coq system. Technical Report RR-6455. INRIA. Available at http://hal.inria.fr/inria-00258384/.
  10. Georges Gonthier, Assia Mahboubi & Enrico Tassi (2015): A Small Scale Reflection Extension for the Coq system. Research Report RR-6455. Inria Saclay Ile de France. Available at https://hal.inria.fr/inria-00258384.
  11. John Harrison (2009): Without Loss of Generality. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Lecture Notes in Computer Science 5674. Springer, pp. 43–59, doi:10.1007/978-3-642-03359-9_3.
  12. J. W. P. Hirschfeld (1985): Finite projective spaces of three dimensions. Oxford mathematical monographs. Clarendon Press ; New York : Oxford University Press, Oxford.
  13. R.H. Jeurissen (1995): Special sets of lines in PG(3, 2). Linear Algebra and its Applications 226-228, pp. 617 – 638, doi:10.1016/0024-3795(95)00200-B. Available at http://www.sciencedirect.com/science/article/pii/002437959500200B. Honoring J.J.Seidel.
  14. Assia Mahboubi & Enrico Tassi (2016): Mathematical Components. Draft. Available at https://math-comp.github.io/mcb/.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org