@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},
)