Martin Aigner & Günter M. Ziegler (2018):
Proofs from THE BOOK,
6th edition.
Springer,
doi:10.1007/978-3-662-57265-8.
Ariane Alves Almeida, Ana Cristina Rocha-Oliveira, Thiago Mendonça Ferreira Ramos, Flávio Leonardo C. de Moura & Mauricio Ayala-Rincón (2019):
The Computational Relevance of Formal Logic Through Formal Proofs.
In: Proceedings 3rd Formal Methods Teaching FMTea,
LNCS 11758.
Springer,
pp. 81–96,
doi:10.1007/978-3-030-32441-4_6.
Jesús Aransay, Clemens Ballarin, Martin Baillon, Paulo Emílio de Vilhena, Stephan Hohe, Florian Kammüller & Lawrence C. Paulson (2019):
The Isabelle/HOL Algebra Library.
Technical Report.
Isabelle Library, University of Cambridge Computer Laboratory and Technische Universität München.
Available at https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/document.pdf.
Mauricio Ayala-Rincón & Flávio Leonardo C. de Moura (2017):
Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs.
UTiCS.
Springer,
doi:10.1007/978-3-319-51653-0.
Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter & Hendrik Spohr (2008):
CERES: An analysis of Fürstenberg's proof of the infinity of primes.
Theor. Comput. Sci. 403(2-3),
pp. 160–175,
doi:10.1016/j.tcs.2008.02.043.
Jonas Bayer, Marco David, Abhik Pal & Benedikt Stock (2019):
Beginners’ Quest to Formalize Mathematics: A Feasibility Study in Isabelle,
pp. 16–27,
doi:10.1007/978-3-030-23250-4_2.
Sandrine Blazy (2019):
Teaching Deductive Verification in Why3 to Undergraduate Students.
In: Proceedings 3rd Formal Methods Teaching FMTea,
LNCS 11758.
Springer,
pp. 52–66,
doi:10.1007/978-3-030-32441-4_4.
Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg & Vincent Siles (2016):
Formalized linear algebra over Elementary Divisor Rings in Coq.
Logical Methods in Computer Science 12(2:7),
pp. 1–23,
doi:10.2168/LMCS-12(2:7)2016.
Cyril Cohen & Assia Mahboubi (2012):
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination.
Logical Methods in Computer Science 8(1:2),
pp. 1–40,
doi:10.2168/LMCS-8(1:2)2012.
Herman Geuvers, Randy Pollack, Freek Wiedijk & Jan Zwanenburg (2002):
A Constructive Algebraic Hierarchy in Coq.
Journal of Symbolic Computation 34(4),
pp. 271–286,
doi:10.1006/jsco.2002.0552.
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi & Laurent Théry (2013):
A Machine-Checked Proof of the Odd Order Theorem.
In: 4th International Conference on Interactive Theorem Proving ITP,
LNCS 7998.
Springer,
pp. 163–179,
doi:10.1007/978-3-642-39634-2_14.
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi & Laurent Théry (2007):
A Modular Formalisation of Finite Group Theory.
In: 20th International Conference Theorem Proving in Higher Order Logics TPHOLs,
LNCS 4732.
Springer,
pp. 86–101,
doi:10.1007/978-3-540-74591-4_8.
John Harrison (2011):
A formal proof of Pick's Theorem.
Math. Struct. Comput. Sci. 21(4),
pp. 715–729,
doi:10.1017/S0960129511000089.
Jónathan Heras, Francisco Jesús Martín-Mateos & Vico Pascual (2015):
Modelling algebraic structures and morphisms in ACL2.
Applicable Algebra in Engineering, Communication and Computing 26(3),
pp. 277–303,
doi:10.1007/s00200-015-0252-9.
Israel (Yitzchak) Nathan Herstein (1975):
Topics in algebra,
2nd edition.
John Wiley & Sons.
Thomas W. Hungerford (1980):
Algebra.
Graduate Texts in Mathematics 73.
Springer,
doi:10.1007/978-1-4612-6101-8.
Reprint of the 1974 original.
Paul Bernard Jackson (1995):
Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra.
Cornell University.
Artur Kornilowicz & Christoph Schwarzweller (2014):
The First Isomorphism Theorem and Other Properties of Rings.
Formalized Mathematics 22(4),
pp. 291– 301,
doi:10.2478/forma-2014-0029.
Thaynara Arielly de Lima, André Luiz Galdino, Andréia B. Avelar & Mauricio Ayala-Rincón (2020):
Formalization of Ring Theory in PVS - Isomorphism Theorems, Principal, Prime and Maximal Ideals,Chinese Remainder Theorem.
Available at http://ayala.mat.unb.br/publications.html.
Jade Philipoom (2018):
Correct-by-Construction Finite Field Arithmetic in Coq.
Master of Engineering in Computer Science, MIT.
Kristin Yvonne Rozier (2019):
On Teaching Applied Formal Methods in Aerospace Engineering.
In: Proceedings 3rd Formal Methods Teaching FMTea,
LNCS 11758.
Springer,
pp. 111–131,
doi:10.1007/978-3-030-32441-4_8.
Christoph Schwarzweller (2003):
The Binomial Theorem for Algebraic Structures.
Journal of Formalized Mathematics 12(3),
pp. 559–564.
Available at http://mizar.org/JFM/Vol12/binom.html.
Andréia B. Avelar da Silva, Thaynara Arielly de Lima & André Luiz Galdino (2018):
Formalizing Ring Theory in PVS.
In: 9th International Conference on Interactive Theorem Proving ITP,
LNCS 10895.
Springer,
pp. 40–47,
doi:10.1007/978-3-319-94821-8_3.