references.bib

  @article{CaretteBigMath,
  title     = {Big Math And The One-Brain Barrier: the Tetrapod Model Of Mathematical Knowledge},
  author    = {Carette, Jacques and Farmer, William M and Kohlhase, Michael and Rabe, Florian},
  journal   = {The Mathematical Intelligencer},
  volume    = {43},
  pages     = {78--87},
  year      = {2021},
  publisher = {Springer}
}
  @misc{BuildingDiamond,
  title   = {Building on the Diamonds between Theories: Theory Presentation Combinators},
  author  = {Jacques Carette and Russell O'Connor and Yasmine Sharoda},
  journal = {arXiv: Logic in Computer Science},
  year    = {2018},
  url     = {https://api.semanticscholar.org/CorpusID:213292558}
}

  @inproceedings{10.1145/3372885.3373824,
  author    = {The mathlib Community},
  title     = {The Lean Mathematical Library},
  year      = {2020},
  isbn      = {9781450370974},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  url       = {https://doi.org/10.1145/3372885.3373824},
  doi       = {10.1145/3372885.3373824},
  abstract  = {This paper describes mathlib, a community-driven effort to build a unified library
               of mathematics formalized in the Lean proof assistant. Among proof assistant libraries,
               it is distinguished by its dependently typed foundations, focus on classical mathematics,
               extensive hierarchy of structures, use of large- and small-scale automation, and distributed
               organization. We explain the architecture and design decisions of the library and
               the social organization that has led to its development.},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  pages     = {367-381},
  numpages  = {15},
  keywords  = {formal library, Lean, mathlib, formal proof},
  location  = {New Orleans, LA, USA},
  series    = {CPP 2020}
}
  @inbook{Paulin-Mohring2012,
  author    = {Paulin Mohring, Christine},
  title     = {Introduction To The Coq Proof-Assistant For Practical Software Verification},
  booktitle = {Tools for Practical Software Verification: LASER, International Summer School 2011, Elba Island, Italy, Revised Tutorial Lectures},
  year      = {2012},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {45--95},
  abstract  = {This paper is a tutorial on using the Coq proof-assistant for reasoning on software correctness. It illustrates features of Coq like inductive definitions and proof automation on a few examples including arithmetic, algorithms on functional and imperative lists and cryptographic protocols.},
  isbn      = {978-3-642-35746-6},
  doi       = {10.1007/978-3-642-35746-6_3},
  url       = {https://doi.org/10.1007/978-3-642-35746-6_3}
}

  @misc{2019arXiv191203028S,
  author        = {{Saqib Nawaz}, M. and {Malik}, Moin and {Li}, Yi and {Sun}, Meng and {Ikram Ullah Lali}, M.},
  title         = {{A Survey On Theorem Provers In Formal Methods}},
  journal       = {arXiv e-prints},
  keywords      = {Computer Science - Software Engineering, Computer Science - Formal Languages and Automata Theory, Computer Science - Logic in Computer Science},
  year          = {2019},
  month         = {December},
  archiveprefix = {arXiv},
  eprint        = {1912.03028},
  primaryclass  = {cs.SE},
  adsurl        = {https://ui.adsabs.harvard.edu/abs/2019arXiv191203028S},
  adsnote       = {Provided by the SAO/NASA Astrophysics Data System}
}
  @book{assia_mahboubi_2021_4457887,
  author    = {Assia Mahboubi and
               Enrico Tassi},
  title     = {Mathematical Components},
  publisher = {Zenodo},
  year      = 2021,
  month     = jan,
  doi       = {10.5281/zenodo.4457887},
  url       = {https://doi.org/10.5281/zenodo.4457887},
  address   = {Online book}
}
  @article{8e96b2c3fc5b44a79ede72c567ae1621,
  title     = {Proof Assistants : History, ideas And Future},
  abstract  = {In this paper I will discuss the fundamental ideas behind proof assistants: What are they and what is a proof anyway? I give a short history of the main ideas, emphasizing the way they ensure the correctness of the mathematics formalized. I will also briefly discuss the places where proof assistants are used and how we envision their extended use in the future. While being an introduction into the world of proof assistants and the main issues behind them, this paper is also a position paper that pushes the further use of proof assistants. We believe that these systems will become the future of mathematics, where definitions, statements, computations and proofs are all available in a computerized form. An important application is and will be in computer supported modelling and verification of systems. But there is still a long road ahead and I will indicate what we believe is needed for the further proliferation of proof assistants. Keywords. Proof assistant; verification; logic; software correctness; formalized mathematics.},
  author    = {J.H. Geuvers},
  year      = {2009},
  doi       = {10.1007/s12046-009-0001-5},
  language  = {English},
  volume    = {34},
  pages     = {3--25},
  journal   = {Sadhana : Academy Proceedings in Engineering Sciences (Indian Academy of Sciences)},
  issn      = {0256-2499},
  publisher = {Springer},
  number    = {1}
}
  @article{kozen1994completeness,
  title     = {A Completeness Theorem For Kleene Algebras And The Algebra Of Regular Events},
  author    = {Kozen, Dexter},
  journal   = {Information and computation},
  volume    = {110},
  number    = {2},
  pages     = {366--390},
  year      = {1994},
  publisher = {Elsevier}
}
  @article{liaqat2021some,
  title     = {Some Important Applications Of Semigroups},
  author    = {Liaqat, Iqra and Younas, Wajeeha},
  journal   = {Journal of Mathematical Sciences \& Computational Mathematics},
  volume    = {2},
  number    = {2},
  pages     = {317--321},
  year      = {2021},
  publisher = {Society for Makers, Artists, Researchers and Technologists}
}
  @article{evans1974identities,
  title     = {Identities And Relations In Commutative Moufang Loops},
  author    = {Evans, Trevor},
  journal   = {Journal of Algebra},
  volume    = {31},
  number    = {3},
  pages     = {508--513},
  year      = {1974},
  publisher = {Academic Press}
}
  @inproceedings{ganascia1993algebraic,
  title        = {Algebraic Structure Of Some Learning Systems},
  author       = {Ganascia, Jean-Gabriel},
  booktitle    = {International Workshop on Algorithmic Learning Theory},
  pages        = {398--409},
  year         = {1993},
  organization = {Springer},
  address      = {Berlin, Heidelberg},
  isbn         = {978-3-540-48096-9},
  publisher    = {Springer Berlin Heidelberg}
}
  
  @article{esik1995equational,
  title     = {Equational Properties Of Kleene Algebras Of Relations With Conversion},
  author    = {{\'E}sik, Zolt{\'a}n and Bern{\'a}tsky, Laszlo},
  journal   = {Theoretical Computer Science},
  volume    = {137},
  number    = {2},
  pages     = {237--251},
  year      = {1995},
  publisher = {Elsevier}
}
  @techreport{broda2014kleene,
  title       = {Kleene Algebra Completeness},
  author      = {Broda, Sabine and Cavadas, S{\'\i}lvia and Moreira, Nelma},
  year        = {2014},
  institution = {Technical report, Universidade de Porto}
}
  @article{jaiyeola2021new,
  title     = {New Algebraic Properties Of Middle Bol Loops Ii},
  author    = {Jaiyeola, Temitope Gbolahan and David, Sunday Peter and Oyebola, Oyeyemi O},
  journal   = {Proyecciones (Antofagasta)},
  volume    = {40},
  number    = {1},
  pages     = {85--106},
  year      = {2021},
  publisher = {SciELO Chile}
}
  @article{kunen1996moufang,
  title     = {Moufang Quasigroups},
  author    = {Kunen, Kenneth},
  journal   = {Journal of Algebra},
  volume    = {183},
  number    = {1},
  pages     = {231--234},
  year      = {1996},
  publisher = {Academic Press}
}
  @article{deng2016characterizations,
  author  = {Deng, Fang'an and Chen, Lu and Tuo, Shouheng and Ren, ShengZhang},
  year    = {2016},
  month   = {01},
  pages   = {1-7},
  title   = {Characterizations of N(2,2,0) Algebras},
  volume  = {2016},
  journal = {Algebra},
  doi     = {10.1155/2016/2752681}
}
  @article{didurik2018some,
  author    = {{Didurik}, Natalia N. and {Shcherbacov}, Victor A.},
  title     = {Some properties of Neumann quasigroups},
  journal   = {Conference on Applied and Industrial Mathematics},
  keywords  = {Mathematics - Group Theory, 20N05},
  year      = {2018},
  number    = {93-94},
  pages     = {1-7},
  volume    = {1},
  publisher = {Instrumental Biometric National}
}
  @article{phillips2010automated,
  title     = {Automated Theorem Proving In Quasigroup And Loop Theory},
  author    = {Phillips, JD and Stanovsk{\`y}, David},
  journal   = {Ai Communications},
  volume    = {23},
  number    = {2-3},
  pages     = {267--283},
  year      = {2010},
  publisher = {IOS Press}
}
  @article{bruck1944some,
  title   = {Some Results In The Theory Of Quasigroups},
  author  = {Bruck, Richard H},
  journal = {Transactions of the American Mathematical Society},
  volume  = {55},
  pages   = {19--52},
  year    = {1944}
}
  @techreport{kang1990feature,
  title       = {Feature-Oriented Domain Analysis (FODA) Feasibility Study},
  author      = {Kang, Kyo C and Cohen, Sholom G and Hess, James A and Novak, William E and Peterson, A Spencer},
  year        = {1990},
  institution = {Carnegie-Mellon Univ Pittsburgh Pa Software Engineering Inst}
}
  @inproceedings{hu2021formalizing,
  author    = {Hu, Jason Z. S. and Carette, Jacques},
  title     = {Formalizing Category Theory in Agda},
  year      = {2021},
  isbn      = {9781450382991},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  url       = {https://doi.org/10.1145/3437992.3439922},
  doi       = {10.1145/3437992.3439922},
  booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  pages     = {327-342},
  numpages  = {16},
  keywords  = {category theory, Agda, formal mathematics},
  location  = {Virtual, Denmark},
  series    = {CPP 2021}
}
  @article{sankappanavar1981course,
  title     = {A Course In Universal Algebra},
  author    = {Sankappanavar, Hanamantagouda P and Burris, Stanley},
  journal   = {Graduate Texts Math},
  volume    = {78},
  pages     = {56},
  year      = {1981},
  publisher = {Citeseer}
}
  @book{russell2020principles,
  title     = {The Principles Of Mathematics},
  author    = {Russell, Bertrand},
  publisher = {Routledge},
  year      = {1939},
  address   = {Online book}
}
  @misc{russelPara,
  author = {Alexander, Katz and Christopher, Williams and Jimin, Khim},
  title  = {Russell'S Paradox},
  year   = {2023},
  url    = {https://brilliant.org/wiki/russells-paradox/},
  note   = {[Online; accessed 16-January-2023]}
}
  @misc{universeagda,
  title  = {Universe Levels},
  author = {{Agda Development Team}},
  url    = {https://agda.readthedocs.io/en/v2.6.1.3/language/universe-levels.html},
  year   = {2023}
} 

  @article{ungar2007einstein,
  title     = {Einstein's Velocity Addition Law And Its Hyperbolic Geometry},
  author    = {Ungar, Abraham A},
  journal   = {Computers \& Mathematics with Applications},
  volume    = {53},
  number    = {8},
  pages     = {1228--1250},
  year      = {2007},
  publisher = {Elsevier}
}

  @article{larchey2020hilbert,
  title    = {Hilbert's Tenth Problem In Coq (Extended Version)},
  author   = {Larchey-Wendling, Dominique and Forster, Yannick},
  journal  = {arXiv preprint arXiv:2003.04604},
  year     = {2020},
  numpages = {41},
  pages    = {1-41},
  volume   = {18}
}
  @article{pedrouzo2021revisiting,
  title     = {Revisiting Multivariate Ring Learning With Errors And Its Applications On Lattice-Based Cryptography},
  author    = {Pedrouzo-Ulloa, Alberto and Troncoso-Pastoriza, Juan Ram{\'o}n and Gama, Nicolas and Georgieva, Mariya and P{\'e}rez-Gonz{\'a}lez, Fernando},
  journal   = {Mathematics},
  volume    = {9},
  number    = {8},
  pages     = {858},
  year      = {2021},
  publisher = {MDPI}
}
  @article{netto2008influence,
  title     = {Influence Of Topology In A Quantum Ring},
  author    = {Netto, AL Silva and Chesman, C and Furtado, Cla{\'u}dio},
  journal   = {Physics Letters A},
  volume    = {372},
  number    = {21},
  pages     = {3894--3897},
  year      = {2008},
  publisher = {Elsevier}
}
  @article{khathuria2021algebraic,
  title     = {On The Algebraic Structure Of E\_p\^{}(M) E p (m) And Applications To Cryptography},
  author    = {Khathuria, Karan and Micheli, Giacomo and Weger, Violetta},
  journal   = {Applicable Algebra in Engineering, Communication and Computing},
  volume    = {32},
  pages     = {495--505},
  year      = {2021},
  publisher = {Springer}
}
  @article{kozen1997kleene,
  title     = {Kleene Algebra With Tests},
  author    = {Kozen, Dexter},
  journal   = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume    = {19},
  number    = {3},
  pages     = {427--443},
  year      = {1997},
  publisher = {ACM New York, NY, USA}
}

  @article{redko1964defining,
  title   = {On Defining Relations For The Algebra Of Regular Events},
  author  = {Redko, Valentin N},
  journal = {Ukrainskii Matematicheskii Zhurnal},
  volume  = {16},
  pages   = {120--126},
  year    = {1964}
}
  @mastersthesis{kidney2020finiteness,
  title  = {Finiteness In Cubical Type Theory},
  author = {Kidney, Donnacha Ois{\'\i}n},
  year   = {2020},
  school = {University College Cork},
  url    = {https://doisinkidney.com/pdfs/masters-thesis.pdf}
}
  @inproceedings{10.1007/978-3-642-03359-9_6,
  author    = {Bove, Ana
               and Dybjer, Peter
               and Norell, Ulf},
  editor    = {Berghofer, Stefan
               and Nipkow, Tobias
               and Urban, Christian
               and Wenzel, Makarius},
  title     = {A Brief Overview Of Agda -- a Functional Language With Dependent Types},
  booktitle = {Theorem Proving in Higher Order Logics},
  year      = {2009},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {73--78},
  isbn      = {978-3-642-03359-9}
}
  @misc{agdaFunction,
  author = {{Agda Development Team}},
  title  = {Agda functions},
  year   = {2022},
  url    = {https://agda.readthedocs.io/en/v2.5.2/language/function-definitions.html},
  note   = {[Online; accessed 21-February-2023]}
}
  @article{DARewriting,
  issn      = {00224812},
  url       = {http://www.jstor.org/stable/2274856},
  abstract  = {We show that the DA-unification problem is undecidable. That is, given two binary function symbols $\bigoplus$ and $\bigotimes$, variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following DA-axioms hold: \begin{align*}(x \bigoplus y) \bigotimes z &= (x \bigotimes z) \bigoplus (y \bigotimes z),\\x \bigotimes (y \bigoplus z) &= (x \bigotimes y) \bigoplus (x \bigotimes z),\\x \bigoplus (y \bigoplus z) &= (x \bigoplus y) \bigoplus z.\end{align*} Two terms are DA-unifiable (i.e. an equation is solvable in DA) if there exist terms to be substituted for their variables such that the resulting terms are equal in the equational theory DA. This is the smallest currently known axiomatic subset of Hilbert's tenth problem for which an undecidability result has been obtained.},
  author    = {J. Siekmann and P. Szabo},
  journal   = {The Journal of Symbolic Logic},
  number    = {2},
  pages     = {402--414},
  publisher = {Association for Symbolic Logic},
  title     = {The Undecidability Of The Da-Unification Problem},
  urldate   = {2023-03-16},
  volume    = {54},
  year      = {1989}
}

  @phdthesis{YSharoda,
  author = {Yasmine Sharoda},
  title  = {Leveraging Information Contained In Theory Presentations},
  year   = {2021},
  url    = {http://hdl.handle.net/11375/26272},
  school = {McMaster University}
}
  @misc{barnett2017roots,
  title  = {The Roots Of Early Group Theory In The Works Of Lagrange},
  author = {Barnett, Janet Heine},
  year   = {2017},
  url    = {https://digitalcommons.ursinus.edu/cgi/viewcontent.cgi?article=1002&context=triumphs_abstract}
}
  @article{plfa22.08,
  title    = {Programming language foundations in Agda},
  journal  = {Science of Computer Programming},
  volume   = {194},
  pages    = {15},
  year     = {2020},
  issn     = {0167-6423},
  doi      = {https://doi.org/10.1016/j.scico.2020.102440},
  url      = {https://www.sciencedirect.com/science/article/pii/S0167642320300502},
  author   = {Wen Kokke and Jeremy G. Siek and Philip Wadler},
  keywords = {Agda, Coq, Lambda calculus, Dependent types}
}

  @mastersthesis{flinn2021algebraic,
  title  = {Algebraic Structures And Variations: From Latin Squares To Lie Quasigroups},
  author = {Flinn, Erik},
  year   = {2021},
  url    = {https://commons.nmu.edu/cgi/viewcontent.cgi?article=1704&context=theses},
  school = {Northern Michigan University}
}

  @misc{abstractAlgebra,
  title  = {Introduction To Abstract Algebra (math 113)},
  author = {Alexander Paulin},
  year   = {2021},
  url    = {https://math.berkeley.edu/~apaulin/AbstractAlgebra},
  school = {University of California, Berkeley}
}

  @book{sannella2012foundations,
  title     = {Foundations Of Algebraic Specification And Formal Software Development},
  author    = {Sannella, Donald and Tarlecki, Andrzej},
  year      = {2012},
  url       = {https://link.springer.com/book/10.1007/978-3-642-17336-3},
  publisher = {Springer Science \& Business Media},
  address   = {Online book}
}

  @book{gries2013logical,
  title     = {A Logical Approach to Discrete Math},
  author    = {Gries, D. and Schneider, F.B.},
  isbn      = {9780387941158},
  lccn      = {lc93027848},
  series    = {Monographs in Computer Science},
  url       = {https://books.google.ca/books?id=ZWTDQ6H6gsUC},
  year      = {1993},
  publisher = {Springer New York},
  address   = {New York}
}

  @phdthesis{musa,
  author = {Al Hassy, Musa},
  title  = {Do-It-Yourself Module Systems},
  year   = {2021},
  url    = {http://hdl.handle.net/11375/26373},
  school = {McMaster University}
}

  @book{wechler2012universal,
  title     = {Universal Algebra for Computer Scientists},
  author    = {Wechler, W.},
  isbn      = {9783642767715},
  series    = {Monographs in Theoretical Computer Science. An EATCS Series},
  url       = {https://books.google.ca/books?id=jUGqCAAAQBAJ},
  year      = {2012},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin Heidelberg}
}

  @misc{AgdaDoc,
  title  = {What is Agda?},
  author = {{Agda Development Team}},
  url    = {https://agda.readthedocs.io/en/v2.6.3/getting-started/what-is-agda.html},
  year   = {2023}
} 

  @book{AgdaTB,
  author    = {Stump, Aaron},
  title     = {Verified Functional Programming in Agda},
  year      = {2016},
  isbn      = {9781970001273},
  publisher = {Association for Computing Machinery and Morgan \& Claypool},
  address   = {Online book}
}
  @inproceedings{al2019language,
  author    = {Al-hassy, Musa and Carette, Jacques and Kahl, Wolfram},
  title     = {A Language Feature to Unbundle Data at Will (Short Paper)},
  year      = {2019},
  isbn      = {9781450369800},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  url       = {https://doi.org/10.1145/3357765.3359523},
  doi       = {10.1145/3357765.3359523},
  booktitle = {Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences},
  pages     = {14-19},
  numpages  = {6},
  keywords  = {extensible, dependent-types, Emacs, packages, modules, Agda, meta-program},
  location  = {Athens, Greece},
  series    = {GPCE 2019}
}
  @phdthesis{coquand1986analysis,
  title  = {An Analysis Of Girard'S Paradox},
  author = {Coquand, Thierry},
  year   = {1986},
  school = {INRIA}
}
  @misc{sortSystem,
  title  = {Sort System},
  author = {{Agda Development Team}},
  url    = {https://agda.readthedocs.io/en/v2.6.3.20230805/language/sort-system.html},
  year   = {2023}
} 
  @book{norell2007towards,
  title     = {Towards A Practical Programming Language Based On Dependent Type Theory},
  author    = {Norell, Ulf},
  volume    = {32},
  year      = {2007},
  publisher = {Chalmers University of Technology},
  address   = {Gothenburg, Sweden}
}
  @misc{bocquet2020coherence,
  title   = {Coherence Of Strict Equalities In Dependent Type Theories},
  author  = {Bocquet, Rafa{\"e}l},
  journal = {arXiv preprint arXiv:2010.14166},
  year    = {2020}
}
  @article{eremondi2022propositional,
  title     = {Propositional Equality For Gradual Dependently Typed Programming},
  author    = {Eremondi, Joseph and Garcia, Ronald and Tanter, {\'E}ric},
  journal   = {Proceedings of the ACM on Programming Languages},
  volume    = {6},
  number    = {ICFP},
  pages     = {165--193},
  year      = {2022},
  publisher = {ACM New York, NY, USA}
}
  @book{martin1984intuitionistic,
  title     = {Intuitionistic Type Theory},
  author    = {Martin-L{\"o}f, Per and Sambin, Giovanni},
  volume    = {9},
  year      = {1984},
  publisher = {Bibliopolis Naples},
  address   = {Online book}
}
  @misc{murray2022constructive,
  title   = {Constructive Analysis In The Agda Proof Assistant},
  author  = {Murray, Zachary},
  journal = {arXiv preprint arXiv:2205.08354},
  year    = {2022}
}
  @misc{abel2012agda,
  title  = {Agda: Equality},
  author = {Abel, Andreas},
  year   = {2012},
  url    = {https://www2.tcs.ifi.lmu.de/~abel/Equality.pdf}
}
  @misc{danielsson2011agda,
  title   = {Agda Standard Library},
  author  = {"The Agda Community"},
  url     = {https://github.com/agda/agda-stdlib},
  version = {v1.7},
  year    = {2022}
}
  @article{Brady2021Idris2Q,
  title   = {Idris 2: quantitative Type Theory In Practice},
  author  = {Brady, Edwin},
  journal = {ArXiv},
  year    = {2021},
  pages   = {27},
  volume  = {abs/2104.00480},
  url     = {https://api.semanticscholar.org/CorpusID:232478760}
}
  @article{kohlhase2021experiences,
  title     = {Experiences From Exporting Major Proof Assistant Libraries},
  author    = {Kohlhase, Michael and Rabe, Florian},
  journal   = {Journal of Automated Reasoning},
  volume    = {65},
  number    = {8},
  pages     = {1265--1298},
  year      = {2021},
  publisher = {Springer}
}
  @book{bertot2013interactive,
  title     = {Interactive Theorem Proving And Program Development: coq'Art: the Calculus Of Inductive Constructions},
  author    = {Bertot, Yves and Cast'eran, Pierre},
  year      = {2013},
  publisher = {Springer Science \& Business Media},
  address   = {Online book}
}
  @book{brady2022idris,
  title     = {Type-driven development with Idris},
  author    = {Brady, Edwin},
  year      = {2017},
  publisher = {Simon and Schuster},
  address   = {Online book}
}
  @article{brady2013idris,
  title     = {Idris, A General-Purpose Dependently Typed Programming Language: Design And Implementation},
  author    = {Brady, Edwin},
  journal   = {Journal of functional programming},
  volume    = {23},
  number    = {5},
  pages     = {552--593},
  year      = {2013},
  publisher = {Cambridge University Press}
}
  @inproceedings{de2015lean,
  title        = {The Lean Theorem Prover (System Description)},
  author       = {de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and Van Doorn, Floris and von Raumer, Jakob},
  booktitle    = {Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25},
  pages        = {378--388},
  year         = {2015},
  publisher    = {Springer},
  url          = {https://link.springer.com/chapter/10.1007/978-3-319-21401-6_26},
  organization = {Springer},
  address      = {Cham},
  isbn         = {978-3-319-21401-6}
}
  @article{ebner2017metaprogramming,
  title     = {A Metaprogramming Framework For Formal Verification},
  author    = {Ebner, Gabriel and Ullrich, Sebastian and Roesch, Jared and Avigad, Jeremy and de Moura, Leonardo},
  journal   = {Proceedings of the ACM on Programming Languages},
  volume    = {1},
  number    = {ICFP},
  pages     = {1--29},
  year      = {2017},
  publisher = {ACM New York, NY, USA}
}
  @article{baanen2022use,
  author        = {{Baanen}, Anne},
  title         = {{Use and abuse of instance parameters in the Lean mathematical library}},
  journal       = {arXiv e-prints},
  keywords      = {Computer Science - Logic in Computer Science, F.4.1},
  year          = 2022,
  month         = feb,
  eid           = {arXiv:2202.01629},
  pages         = {1-20},
  volume        = {1},
  numpages      = {20},
  doi           = {10.48550/arXiv.2202.01629},
  archiveprefix = {arXiv},
  number        = {2202.01629},
  primaryclass  = {cs.LO},
  url           = {https://ui.adsabs.harvard.edu/abs/2022arXiv220201629B},
  adsnote       = {Provided by the SAO/NASA Astrophysics Data System}
}
  @techreport{Stener2016MoufangL,
  author      = {Stener, Mikael},
  institution = {Uppsala University, Algebra and Geometry},
  pages       = {49},
  school      = {Uppsala University, Algebra and Geometry},
  title       = {Moufang Loops : General theory and visualization of non-associative Moufang loops of order 16},
  series      = {U.U.D.M. project report},
  number      = {2016:18},
  year        = {2016}
}

  @inproceedings{khan2015mining,
  title        = {A Mining Based Approach For Efficient Enumeration Of Algebraic Structures},
  author       = {Khan, Majid Ali and Mohammad, Nazeeruddin and Muhammad, Shahabuddin and Ali, Asif},
  booktitle    = {2015 IEEE International Conference on Data Science and Advanced Analytics (DSAA)},
  pages        = {1--6},
  publisher    = {IEEE},
  year         = {2015},
  address      = {Greece},
  organization = {IEEE}
}
  @article{anh1987morita,
  title     = {Morita Equivalence For Rings Without Identity},
  author    = {{\'A}nh, PN and M{\'a}rki, L},
  journal   = {Tsukuba journal of mathematics},
  volume    = {11},
  number    = {1},
  pages     = {1--16},
  year      = {1987},
  publisher = {JSTOR}
}
  @book{jacobson1956structure,
  title     = {Structure of Rings},
  author    = {Jacobson, N.},
  isbn      = {9780821810378},
  lccn      = {lc63021795},
  series    = {American Mathematical Society colloquium publications: vol. 37},
  url       = {https://books.google.ca/books?id=KwviDgAAQBAJ},
  year      = {1964},
  publisher = {American Mathematical Society},
  address   = {Rhode Island, United States}
}

  @article{persson1999application,
  title     = {An Application Of The Constructive Spectrum Of A Ring},
  author    = {Persson, Henrik},
  journal   = {Type Theory and the Integrated Logic of Programs. Chalmers University and University of G{\"o}teborg},
  year      = {1999},
  volume    = {1},
  numpages  = {19},
  pages     = {1=19},
  publisher = {Citeseer}
}
  @article{lehmann1977algebraic,
  title     = {Algebraic Structures For Transitive Closure},
  author    = {Lehmann, Daniel J},
  journal   = {Theoretical Computer Science},
  volume    = {4},
  number    = {1},
  pages     = {59--76},
  year      = {1977},
  publisher = {Elsevier}
}
  @article{geuvers2002constructive,
  title     = {A Constructive Algebraic Hierarchy In Coq},
  author    = {Geuvers, Herman and Pollack, Randy and Wiedijk, Freek and Zwanenburg, Jan},
  journal   = {Journal of Symbolic Computation},
  volume    = {34},
  number    = {4},
  pages     = {271--286},
  year      = {2002},
  publisher = {Elsevier}
}
  @book{shcherbacov2003elements,
  author    = {Shcherbacov, Victor},
  title     = {Elements of Quasigroup Theory and Applications},
  year      = {2017},
  isbn      = {1498721559},
  publisher = {Chapman \& Hall/CRC},
  edition   = {1st},
  address   = {Online book}
}
  @book{lam1991first,
  title     = {A First Course In Noncommutative Rings},
  author    = {Lam, Tsit-Yuen},
  volume    = {131},
  year      = {1991},
  publisher = {Springer},
  address   = {New York}
}
  @book{grove2012algebra,
  title     = {Algebra},
  author    = {Grove, Larry C},
  year      = {2012},
  publisher = {Courier Corporation},
  address   = {Online book}
}
  @article{bosma1997magma,
  title     = {The Magma Algebra System I: the User Language},
  author    = {Bosma, Wieb and Cannon, John and Playoust, Catherine},
  journal   = {Journal of Symbolic Computation},
  volume    = {24},
  number    = {3-4},
  pages     = {235--265},
  year      = {1997},
  publisher = {Elsevier}
}
  @article{rasuli2022anti,
  title     = {Anti-Fuzzy Bi-Ideals In Semirings Under S-Norms},
  author    = {Rasuli, Rasul},
  journal   = {Fuzzy Optimization and Modeling Journal},
  volume    = {3},
  number    = {4},
  pages     = {19--31},
  year      = {2022},
  publisher = {Islamic Azad University, Qaemshahr Branch}
}
  @article{desharnais2004modal,
  author  = {Desharnais, Jules and Möller, Bernhard and Struth, Georg},
  year    = {2004},
  month   = {04},
  pages   = {93-131},
  title   = {Modal Kleene Algebra And Applications - A Survey},
  volume  = {1},
  journal = {Journal of Relational Methods in Computer SAcience}
}
  @phdthesis{ulus2018pattern,
  title  = {Pattern Matching With Time: theory And Applications},
  author = {Ulus, Dogan},
  year   = {2018},
  school = {Universite Grenoble Alpes}
}
  @book{judson2020abstract,
  title     = {Abstract Algebra: theory And Applications},
  author    = {Judson, Thomas W},
  year      = {2020},
  publisher = {Orthogonal Publishing},
  address   = {Online book}
}

  @misc{directproduct,
  title     = {Direct product and Direct Sum},
  author    = {R.A Bailey},
  publisher = {Queen Mary University of London},
  pages     = {4},
  url       = {https://webspace.maths.qmul.ac.uk/r.a.bailey/MAS305/algnotes14.pdf},
  year      = {2023}
}
  @book{szabo2000linear,
  title     = {Linear Algebra with Mathematica: An Introduction Using Mathematica},
  author    = {Szabo, Fred},
  year      = {2000},
  publisher = {Academic Press},
  address   = {Online book}
}