@book(theBook2018,
 author       = {Martin Aigner and G\"{u}nter M. Ziegler},
 year         = {2018},
 title        = {{Proofs from THE BOOK}},
 edition      = {6th},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-57265-8},
)
@inproceedings(AR_FMTeaching2019,
 author       = {Ariane Alves Almeida and Rocha-Oliveira, Ana Cristina and Ferreira Ramos, Thiago Mendon\c{c}a and Fl\'avio Leonardo C. de Moura and Ayala-Rinc\'on, Mauricio},
 year         = {2019},
 title        = {{The Computational Relevance of Formal Logic Through Formal Proofs}},
 booktitle    = {Proceedings 3rd Formal Methods Teaching {FMTea}},
 series       = {LNCS},
 volume       = {11758},
 publisher    = {Springer},
 pages        = {81--96},
 doi          = {10.1007/978-3-030-32441-4\_6},
)
@techreport(ballarinizabelle2019,
 author       = {Jes\'{u}s Aransay and Clemens Ballarin and Martin Baillon and Paulo Em\'{i}lio de Vilhena and Stephan Hohe and Florian Kamm\"{u}ller and Lawrence C. Paulson},
 year         = {2019},
 title        = {{The Isabelle/HOL Algebra Library}},
 type         = {Technical Report},
 institution  = {Isabelle Library, University of Cambridge Computer Laboratory and Technische Universit\"at M\"unchen},
 url          = {https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/document.pdf},
)
@book(ayala2017applied,
 author       = {Ayala-Rinc{\'o}n, Mauricio and Fl\'avio Leonardo C. de Moura},
 year         = {2017},
 title        = {{Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs}},
 series       = {{UTiCS}},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-51653-0},
)
@article(BaazHLRS08,
 author       = {Matthias Baaz and Stefan Hetzl and Alexander Leitsch and Clemens Richter and Hendrik Spohr},
 year         = {2008},
 title        = {{CERES:} An analysis of F{\"{u}}rstenberg's proof of the infinity of primes},
 journal      = {Theor. Comput. Sci.},
 volume       = {403},
 number       = {2-3},
 pages        = {160--175},
 doi          = {10.1016/j.tcs.2008.02.043},
)
@inbook(Bayer2019,
 author       = {Jonas Bayer and Marco David and Abhik Pal and Benedikt Stock},
 year         = {2019},
 title        = {{Beginners’ Quest to Formalize Mathematics: A Feasibility Study in Isabelle}},
 pages        = {16--27},
 doi          = {10.1007/978-3-030-23250-4\_2},
)
@inproceedings(Blazy_FMTea2019,
 author       = {Sandrine Blazy},
 year         = {2019},
 title        = {{Teaching Deductive Verification in Why3 to Undergraduate Students}},
 booktitle    = {Proceedings 3rd Formal Methods Teaching {FMTea}},
 series       = {LNCS},
 volume       = {11758},
 publisher    = {Springer},
 pages        = {52--66},
 doi          = {10.1007/978-3-030-32441-4\_4},
)
@misc(PVSalgebra,
 author       = {Ricky Butler and David Lester},
 year         = {2007},
 title        = {{A PVS \emph{Theory} for Abstract Algebra}},
 url          = {https://github.com/nasa/pvslib/tree/pvs7.0/algebra},
 note         = {Accessed in June 17, 2020},
)
@article(cohencoq16,
 author       = {Guillaume Cano and Cyril Cohen and Maxime D\'{e}n\`{e}s and Anders M\"{o}rtberg and Vincent Siles},
 year         = {2016},
 title        = {{Formalized linear algebra over Elementary Divisor Rings in {Coq}}},
 journal      = {Logical Methods in Computer Science},
 volume       = {12},
 number       = {2:7},
 pages        = {1--23},
 doi          = {10.2168/LMCS-12(2:7)2016},
)
@article(Cohen2012,
 author       = {Cyril Cohen and Assia Mahboubi},
 year         = {2012},
 title        = {{Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination}},
 journal      = {Logical Methods in Computer Science},
 volume       = {8},
 number       = {1:2},
 pages        = {1--40},
 doi          = {10.2168/LMCS-8(1:2)2012},
)
@inproceedings(Dubois_FMTea2019,
 author       = {Catherine Dubois and Virgile Prevosto and Guillaume Burel},
 year         = {2019},
 title        = {{Teaching Formal Methods to Future Engineers}},
 booktitle    = {Proceedings 3rd Formal Methods Teaching {FMTea}},
 series       = {LNCS},
 volume       = {11758},
 publisher    = {Springer},
 pages        = {69--80},
 doi          = {10.1007/978-3-030-32441-4\_5},
)
@article(Eberl20a,
 author       = {Manuel Eberl},
 year         = {2020},
 title        = {{F\"urstenberg's topology and his proof of the infinitude of primes}},
 journal      = {Arch. Formal Proofs},
 volume       = {2020},
 url          = {https://www.isa-afp.org/entries/Furstenberg\_Topology.html},
)
@book(Fraleigh,
 author       = {John B. Fraleigh},
 year         = {2002},
 title        = {{A First Course in Abstract Algebra}},
 edition      = {7th},
 publisher    = {Pearson},
)
@article(Fuerstenberg1955,
 author       = {Hillel F\"urstenberg},
 year         = {1955},
 title        = {{On the Infinitude of Primes}},
 journal      = {Amer. Math, Monthly},
 volume       = {62},
 number       = {5},
 pages        = {353},
 doi          = {10.2307/2307043},
)
@misc(PVSgroups,
 author       = {Andr{\'{e}} Luiz Galdino},
 year         = {2011},
 title        = {{A PVS \emph{Theory} for Groups}},
 url          = {https://github.com/nasa/pvslib/tree/pvs7.0/groups},
 note         = {Accessed in June 17, 2020},
)
@article(geuverscoq2002,
 author       = {Herman Geuvers and Randy Pollack and Freek Wiedijk and Jan Zwanenburg},
 year         = {2002},
 title        = {A Constructive Algebraic Hierarchy in {Coq}},
 journal      = {Journal of Symbolic Computation},
 volume       = {34},
 number       = {4},
 pages        = {271--286},
 doi          = {10.1006/jsco.2002.0552},
)
@inproceedings(Gonthier13,
 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 Russell O'Connor 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    = {4th International Conference on Interactive Theorem Proving {ITP}},
 series       = {LNCS},
 volume       = {7998},
 publisher    = {Springer},
 pages        = {163--179},
 doi          = {10.1007/978-3-642-39634-2\_14},
)
@inproceedings(Gonthier2007,
 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}},
 booktitle    = {20th International Conference Theorem Proving in Higher Order Logics {TPHOLs}},
 series       = {LNCS},
 volume       = {4732},
 publisher    = {Springer},
 pages        = {86--101},
 doi          = {10.1007/978-3-540-74591-4\_8},
)
@article(Harrison11,
 author       = {John Harrison},
 year         = {2011},
 title        = {{A formal proof of Pick's Theorem}},
 journal      = {Math. Struct. Comput. Sci.},
 volume       = {21},
 number       = {4},
 pages        = {715--729},
 doi          = {10.1017/S0960129511000089},
)
@article(heras15,
 author       = {J{\'o}nathan Heras and Mart{\'i}n-Mateos, Francisco Jes{\'u}s 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},
)
@book(herstein75,
 author       = {Israel (Yitzchak) Nathan Herstein},
 year         = {1975},
 title        = {Topics in algebra},
 edition      = {2nd},
 publisher    = {John Wiley \& Sons},
)
@book(hungerford80,
 author       = {Thomas W. Hungerford},
 year         = {1980},
 title        = {Algebra},
 series       = {Graduate Texts in Mathematics},
 volume       = {73},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4612-6101-8},
 note         = {Reprint of the 1974 original},
)
@phdthesis(jackson1995,
 author       = {Paul Bernard Jackson},
 year         = {1995},
 title        = {{Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra}},
 school       = {Cornell University},
)
@article(Kornilowicz2014,
 author       = {Artur Kornilowicz and Christoph Schwarzweller},
 year         = {2014},
 title        = {{The First Isomorphism Theorem and Other Properties of Rings}},
 journal      = {Formalized Mathematics},
 volume       = {22},
 number       = {4},
 pages        = {291-- 301},
 doi          = {10.2478/forma-2014-0029},
)
@unpublished(LGAA2020,
 author       = {Thaynara Arielly de Lima and Andr{\'{e}} Luiz Galdino and Andr{\'{e}}ia B. Avelar and Ayala-Rinc{\'{o}}n, Mauricio},
 year         = {2020},
 title        = {Formalization of Ring Theory in PVS - Isomorphism Theorems, Principal, Prime and Maximal Ideals,Chinese Remainder Theorem},
 url          = {http://ayala.mat.unb.br/publications.html},
)
@mastersthesis(Philipoom2018,
 author       = {Jade Philipoom},
 year         = {2018},
 title        = {{Correct-by-Construction Finite Field Arithmetic in Coq}},
 school       = {Master of Engineering in Computer Science, MIT},
)
@inproceedings(Rozier_FMTea2019,
 author       = {Kristin Yvonne Rozier},
 year         = {2019},
 title        = {{On Teaching Applied Formal Methods in Aerospace Engineering}},
 booktitle    = {Proceedings 3rd Formal Methods Teaching {FMTea}},
 series       = {LNCS},
 volume       = {11758},
 publisher    = {Springer},
 pages        = {111--131},
 doi          = {10.1007/978-3-030-32441-4\_8},
)
@article(cs01,
 author       = {Christoph Schwarzweller},
 year         = {2003},
 title        = {{The Binomial Theorem for Algebraic Structures}},
 journal      = {Journal of Formalized Mathematics},
 volume       = {12},
 number       = {3},
 pages        = {559--564},
 url          = {http://mizar.org/JFM/Vol12/binom.html},
)
@inproceedings(SilvaLG18,
 author       = {Andr{\'{e}}ia B. Avelar da Silva and Thaynara Arielly de Lima and Andr{\'{e}} Luiz Galdino},
 year         = {2018},
 title        = {Formalizing Ring Theory in {PVS}},
 booktitle    = {9th International Conference on Interactive Theorem Proving {ITP}},
 series       = {LNCS},
 volume       = {10895},
 publisher    = {Springer},
 pages        = {40--47},
 doi          = {10.1007/978-3-319-94821-8\_3},
)