@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},
)
@article(DBLP:journals/dcc/Betten16,
 author       = {Anton Betten},
 year         = {2016},
 title        = {The packings of PG(3, 3)},
 journal      = {Designs, Codes and Cryptography},
 volume       = {79},
 number       = {3},
 pages        = {583--595},
 doi          = {10.1007/s10623-015-0074-6},
)
@inproceedings(BMS18b,
 author       = {David Braun and Nicolas Magaud and Pascal Schreck},
 year         = {2018},
 title        = {{Formalizing Some "Small" Finite Models of Projective Geometry in Coq}},
 editor       = {Jacques Fleuriot and Dongming Wang and Jacques Calmet},
 booktitle    = {{Proceedings of Artificial Intelligence and Symbolic Computation 2018 (AISC'2018)}},
 series       = {LNAI},
 volume       = {11110},
 pages        = {54--69},
 doi          = {10.1007/978-3-319-99957-9\_4},
 url          = {https://hal.inria.fr/hal-01835493},
)
@article(BRUCK196485,
 author       = {R.H Bruck and R.C Bose},
 year         = {1964},
 title        = {The construction of translation planes from projective spaces},
 journal      = {Journal of Algebra},
 volume       = {1},
 number       = {1},
 pages        = {85--102},
 doi          = {10.1016/0021-8693(64)90010-9},
)
@book(Buekenhout95,
 editor       = {Francis Buekenhout},
 year         = {1995},
 title        = {{Handbook of Incidence Geometry}},
 publisher    = {North Holland},
)
@article(cole1922,
 author       = {F. N. Cole},
 year         = {1922},
 title        = {Kirkman parades},
 journal      = {Bull. Amer. Math. Soc.},
 volume       = {28},
 number       = {9},
 pages        = {435--437},
 doi          = {10.1090/S0002-9904-1922-03599-9},
 url          = {https://projecteuclid.org:443/euclid.bams/1183485271},
)
@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},
)
@book(coxeter,
 author       = {Harold Scott Macdonald Coxeter},
 year         = {2003},
 title        = {{Projective Geometry}},
 publisher    = {Springer Science \& Business Media},
)
@techreport(GM08,
 author       = {Georges Gonthier and Assia Mahboubi},
 year         = {2008},
 title        = {{A Small Scale Reflection Extension for the Coq system}},
 type         = {Technical Report},
 number       = {{RR}-6455},
 institution  = {INRIA},
 url          = {http://hal.inria.fr/inria-00258384/},
)
@techreport(gonthier:inria-00258384,
 author       = {Georges Gonthier and Assia Mahboubi and Enrico Tassi},
 year         = {2015},
 title        = {A Small Scale Reflection Extension for the Coq system},
 type         = {Research Report},
 number       = {RR-6455},
 institution  = {{Inria Saclay Ile de France}},
 url          = {https://hal.inria.fr/inria-00258384},
)
@inproceedings(DBLP:conf/tphol/Harrison09,
 author       = {John Harrison},
 year         = {2009},
 title        = {Without Loss of Generality},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {43--59},
 doi          = {10.1007/978-3-642-03359-9\_3},
)
@book(HirschfeldJ.W.P.JamesWilliamPeter1985Fpso,
 author       = {J. W. P. Hirschfeld},
 year         = {1985},
 title        = {Finite projective spaces of three dimensions},
 series       = {Oxford mathematical monographs},
 publisher    = {Clarendon Press ; New York : Oxford University Press},
 address      = {Oxford},
)
@article(JEURISSEN1995617,
 author       = {R.H. Jeurissen},
 year         = {1995},
 title        = {{Special sets of lines in PG(3, 2)}},
 journal      = {Linear Algebra and its Applications},
 volume       = {226-228},
 pages        = {617 -- 638},
 doi          = {10.1016/0024-3795(95)00200-B},
 url          = {http://www.sciencedirect.com/science/article/pii/002437959500200B},
 note         = {Honoring J.J.Seidel},
)
@book(math-components,
 author       = {Assia Mahboubi and Enrico Tassi},
 year         = {2016},
 title        = {{Mathematical Components}},
 publisher    = {Draft},
 url          = {https://math-comp.github.io/mcb/},
)