@inproceedings(gonthier,
 author       = {Georges Gonthier and Andrea Asperti and Jeremy Avigad and Yves Bertot and Cyril Cohen and Fran\c{c}ois Garillot and St\'{e}phane Le Roux and Assia Mahboubi and O\IeC{\textquoteright}Connor, Russell and Sidi Ould Biha and Ioana Pasca and Laurence Rideau and Alexey Solovyev and Enrico Tassi and Laurent Th\'{e}ry},
 year         = {2013},
 title        = {A Machine-Checked Proof of the Odd Order Theorem},
 booktitle    = {International Conference on Interactive Theorem Proving},
 pages        = {163--179},
 doi          = {10.1017/S0960129511000132},
)
@techreport(georges,
 author       = {Georges Gonthier and Assia Mahboubi and Laurence Rideau and Enrico Tassi and Laurent Th\'{e}ry},
 year         = {2007},
 title        = {A Modular Formalisation of Finite Group Theory},
 type         = {Technical Report},
 number       = {RR-6156},
 institution  = {Inria},
)
@article(heras,
 author       = {J\IeC{\'o}nathan Heras and Mart\IeC{\'\i}n-Mateos, Francisco and Vico Pascual},
 year         = {2015},
 title        = {Modelling Algebraic Structures and Morphisms in ACL2},
 journal      = {Applicable algebra in engineering, communication and computing},
 volume       = {26},
 number       = {3},
 pages        = {277--303},
 doi          = {10.1007/s00200-015-0252-9},
)
@inproceedings(krug,
 author       = {Warren Hunt and Robert Krug and J Moore},
 year         = {2003},
 title        = {Linear and Nonlinear Arithmetic in ACL2},
 editor       = {Daniel Geist and Enrico Tronci},
 booktitle    = {Correct Hardware Design and Verification Methods},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {319--333},
 doi          = {10.1145/2422.322411},
)
@book(rotman,
 author       = {Joseph Rotman},
 year         = {1965},
 title        = {The Theory of Groups: An Introduction},
 publisher    = {Allyn and Bacon},
)
@misc(eric,
 author       = {Eric Smith},
 title        = {A Formalization of Groups},
 note         = {{\tt books/kestrel/algebra/groups-encap.lisp}, ACL2 repository},
)
@article(yu,
 author       = {Yuan Yu},
 year         = {1990},
 title        = {Computer Proofs in Group Theory},
 journal      = {Journal of Automated Reasoning},
 volume       = {6},
 number       = {3},
 doi          = {10.1007/BF00244488},
)