@article{Solin11,
  author    = {Solin, K.},
  title     = {Normal forms in total correctness for while programs and
               action systems},
  journal   = {J. Logic and Algebraic Programming},
  volume    = {80},
  number    = {6},
  year      = {2011},
  pages     = {362--375}
}

@inproceedings{Wright02,
  author    = {von Wright, J.},
  title     = {From {K}leene Algebra to Refinement Algebra},
  editor    = {Boiten, E. A. and
               M{\"o}ller, B.},
  booktitle = {MPC},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2386},
  year      = {2002},
  pages     = {233--262}
}

@inproceedings{armstrongstruth12hoka,
  author    = {Alasdair Armstrong and
               Georg Struth},
  title     = {Automated Reasoning in Higher-Order Regular Algebra},
  booktitle = {RAMICS 2012},
  year      = {2012},
  pages     = {66-81},
  ee        = {https://doi.org/10.1007/978-3-642-33314-9_5},
  editor    = {Wolfram Kahl and
               Timothy G. Griffin},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7560},
}

@inproceedings{bachmair86commutation,
  author    = {Leo Bachmair and Nachum Dershowitz},
  title     = {Commutation, Transformation, and Termination},
  editor    = {J{\"o}rg H. Siekmann},
  booktitle = {Conference on Automated Deduction},
  volume    = {230},
  series    = {Lecture Notes in Computer Science},
  pages     = {5--20},
  publisher = {Springer},
  year      = {1986},
  ee        = {https://doi.org/10.1007/3-540-16780-3_76}
}

@Book{birkhoff67lattices,
  author =    {Garrett Birkhoff},
  title =        {Lattice Theory},
  publisher =    {American Mathematical Society Colloquium Publications},
  year =         1967}

@Article{boffa90remarque,
  author =       {Maurice Boffa},
  title =        {Une remarque sur les syst\`emes complets
                  d'identit\'es rationnelles},
  journal =      {Informatique The\'eorique et Applications},
  year =         1990,
  volume =    24,
  number =    4,
  pages =     {419--423}}


@inproceedings{cohen00omega,
  author    = {Ernie Cohen},
  title     = {Separation and Reduction},
  booktitle = {MPC},
  year      = {2000},
  pages     = {45--59},
  ee        = {https://doi.org/10.1007/10722010_4},
  editor    = {Roland Carl Backhouse and
               Jos{\'e} Nuno Oliveira},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1837},
}

@book{conway71regular,
  author    = {Conway, John Horton},
  title     = {Regular Algebra and Finite Machines},
  publisher = {Chapman and Hall},
  year      = {1971}
}

@inproceedings{dershowitz09lazy,
  author    = {Nachum Dershowitz},
  title     = {On Lazy Commutation},
  editor    = {Orna Grumberg and
               Michael Kaminski and
               Shmuel Katz and
               Shuly Wintner},
  booktitle = {Languages: From Formal to Natural},
  volume    = {5533},
  series    = {Lecture Notes in Computer Science},
  pages     = {59--82},
  publisher = {Springer},
  year      = {2009},
  ee        = {https://doi.org/10.1007/978-3-642-01748-3_5}
}

@article{desharnaismoellerstruth06kad,
  author    = {Jules Desharnais and
               Bernhard M{\"o}ller and
               Georg Struth},
  title     = {{Kleene} Algebra with Domain},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {7},
  number    = {4},
  year      = {2006},
  pages     = {798-833},
  ee        = {http://doi.acm.org/10.1145/1183278.1183285},
}

@article{doornbos97calculational,
  author    = {Henk Doornbos and
               Roland Carl Backhouse and
               Jaap van der Woude},
  title     = {A Calculational Approach to Mathematical Induction},
  journal   = {Theor. Comput. Sci.},
  volume    = {179},
  number    = {1--2},
  year      = {1997},
  pages     = {103--135},
  ee        = {https://doi.org/10.1016/S0304-3975(96)00154-5}
}


@inproceedings{fosterstruth12regalg,
  author    = {Simon Foster and
               Georg Struth},
  title     = {Automated Analysis of Regular Algebra},
  booktitle = {IJCAR 2012},
  year      = {2012},
  pages     = {271--285},
  ee        = {https://doi.org/10.1007/978-3-642-31365-3_22},
  editor    = {Bernhard Gramlich and
               Dale Miller and
               Uli Sattler},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7364},
}

@inproceedings{fosterstruthweber11tutorial,
  author    = {Simon Foster and
               Georg Struth and
               Tjark Weber},
  title     = {Automated Engineering of Relational and Algebraic Methods
               in {Isabelle}/{HOL} -- (Invited Tutorial)},
  booktitle = {RAMICS},
  year      = {2011},
  editor    = {Harrie C. M. de Swart},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6663},
  pages     = {52--67},
  ee        = {https://doi.org/10.1007/978-3-642-21070-9_5},

}

@Book{galatosjipsenkowalskiono07residuated,
  author =    {Nikolaos Galatos and Peter Jipsen and Tomasz Kowalski and Hiroakira Ono},
  title =        {Resituated Lattices: An Algebraic Glimpse at Substructural Logics},
  publisher =    {Elsevier},
  year =         2007}

@book{gondran10graphs,
  author    = {Michel Gondran and Michel Minoux},
  title     = {Graphs, Dioids and Semirings: New Models and Algorithms},
  volume    = {41},
  series    = {Operations Research/Computer Science Interfaces},
  publisher = {Springer},
  year      = {2010}
}

@inproceedings{guttmannstruthweber11algmeth,
  author    = {Walter Guttmann and
               Georg Struth and
               Tjark Weber},
  title     = {Automating Algebraic Methods in {Isabelle}},
  booktitle = {ICFEM 2011},
  year      = {2011},
  pages     = {617-632},
  ee        = {https://doi.org/10.1007/978-3-642-24559-6_41},
  editor    = {Shengchao Qin and
               Zongyan Qiu},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6991},
 }

@inproceedings{guttmannstruthweber11tarskikleene,
  author    = {Walter Guttmann and
               Georg Struth and
               Tjark Weber},
  title     = {A Repository for {Tarski}-{Kleene} Algebras},
  booktitle = {ATE 2011},
  year      = {2011},
  pages     = {30--39},
  ee        = {http://ceur-ws.org/Vol-760/paper5.pdf},
  editor    = {Peter H{\"o}fner and
               Annabelle McIver and
               Georg Struth},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = {760},
}

@Book{harelkozentiuryn00dynamic,
  author =    {David Haren and Dexter Kozen and Jerzy Tiuryn},
  title =        {Dynamic Logic},
  publisher =    {MIT Press},
  year =         2000}

@article{hofnerstruth10nontermination,
  author    = {Peter H{\"o}fner and
               Georg Struth},
  title     = {Algebraic notions of nontermination: Omega and divergence
               in idempotent semirings},
  journal   = {J. Log. Algebr. Program.},
  volume    = {79},
  number    = {8},
  year      = {2010},
  pages     = {794-811},
  ee        = {https://doi.org/10.1016/j.jlap.2010.07.016},
}

@Article{kad,
  author = 	 {Gomes, Victor B. F. and Guttmann, W. and H{\"o}fner, P. and Struth, G. and Weber, T.},
  title = 	 {Kleene Algebra with Domain},
  journal = 	 {Archive of Formal Proofs},
  year = 	 2016}

@Article{kat,
  author = 	 {Armstrong, A. and Gomes, Victor B. F. and Struth, G.},
  title = 	 {Kleene Algebra with Tests},
  journal = 	 {Archive of Formal Proofs},
  year = 	 2014}


@article{kozen00hoare,
  author    = {Dexter Kozen},
  title     = {On {Hoare} logic and {Kleene} algebra with tests},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {1},
  number    = {1},
  year      = {2000},
  pages     = {60--76},
  ee        = {https://doi.org/10.1145/343369.343378}
}

@inproceedings{kozen90kleene,
  author    = {Dexter Kozen},
  title     = {On {Kleene} Algebras and Closed Semirings},
  editor    = {Branislav Rovan},
  booktitle = {Mathematical Foundations of Computer Science},
  volume    = {452},
  series    = {Lecture Notes in Computer Science},
  pages     = {26--47},
  publisher = {Springer},
  year      = {1990},
  ee        = {https://doi.org/10.1007/BFb0029594}
}

@article{kozen94complete,
  author    = {Dexter Kozen},
  title     = {A Completeness Theorem for {Kleene} Algebras and the Algebra
               of Regular Events},
  journal   = {Inf. Comput.},
  volume    = {110},
  number    = {2},
  year      = {1994},
  pages     = {366-390},
  ee        = {https://doi.org/10.1006/inco.1994.1037},
}

@article{krauss12regular,
  author    = {Alexander Krauss and
               Tobias Nipkow},
  title     = {Proof Pearl: Regular Expression Equivalence and Relation
               Algebra},
  journal   = {J. Autom. Reasoning},
  volume    = {49},
  number    = {1},
  year      = {2012},
  pages     = {95--106},
  ee        = {https://doi.org/10.1007/s10817-011-9223-4}
}

@inproceedings{mciverweber05pka,
  author    = {Annabelle McIver and
               Tjark Weber},
  title     = {Towards Automated Proof Support for Probabilistic Distributed
               Systems},
  booktitle = {LPAR},
  series    = {Lecture Notes in Computer Science},
  volume    = {3835},
  year      = {2005},
  editor    = {Geoff Sutcliffe and Andrei Voronkov},
  pages     = {534--548},

}

@book{pilz83nearrings,
  author    = {G{\"u}nter Pilz},
  title     = {Near-rings},
  publisher = {North-Holland},
  address   = {Amsterdam},
  edition   = {Second},
  year      = {1983}
}

@inproceedings{pratt90action,
  author    = {Vaughan R. Pratt},
  title     = {Action Logic and Pure Induction},
  editor    = {Jan van Eijck},
  booktitle = {Logics in AI, European Workshop, JELIA '90},
  volume    = {478},
  series    = {Lecture Notes in Computer Science},
  pages     = {97--120},
  publisher = {Springer},
  year      = {1991},
  ee        = {https://doi.org/10.1007/BFb0018436}
}

@Article{regalg,
  author = 	 {Foster, S. and Struth, G.},
  title = 	 {Regular Algebras},
  journal = 	 {Archive of Formal Proofs},
  year = 	 2014}

@Article{rel,
  author = 	 {Armstrong, A. and Foster, S. and Guttmann, W. and Struth, G. and Weber, T.},
  title = 	 {Relation Algebra},
  journal = 	 {Archive of Formal Proofs},
  year = 	 2014}

@article{struth06churchrosser,
  author    = {Georg Struth},
  title     = {Abstract abstract reduction},
  journal   = {J. Log. Algebr. Program.},
  volume    = {66},
  number    = {2},
  year      = {2006},
  pages     = {239-270},
  ee        = {https://doi.org/10.1016/j.jlap.2005.04.001},
}

@article{struth12regeq,
  author    = {Georg Struth},
  title     = {Left omega algebras and regular equations},
  journal   = {J. Log. Algebr. Program.},
  volume    = {81},
  number    = {6},
  year      = {2012},
  pages     = {705-717},
  ee        = {https://doi.org/10.1016/j.jlap.2012.05.004},
}

@article{venema03gamealgebra,
  author    = {Yde Venema},
  title     = {Representation of Game Algebras},
  journal   = {Studia Logica},
  volume    = {75},
  number    = {2},
  year      = {2003},
  pages     = {239-256},
  ee        = {https://doi.org/10.1023/A:1027363028181},
}

@article{vonwright04refinement,
  author    = {Joakim von Wright},
  title     = {Towards a refinement algebra},
  journal   = {Science of Computer Programming},
  volume    = {51},
  number    = {1--2},
  year      = {2004},
  pages     = {23--45},
  ee        = {https://doi.org/10.1016/j.scico.2003.09.002},
}

@article{wagner77omega,
  author    = {Klaus W. Wagner},
  title     = {Eine topologische {C}harakterisierung einiger {K}lassen regul{\"a}rer
               {F}olgenmengen},
  journal   = {Elektronische Informationsverarbeitung und Kybernetik},
  volume    = {13},
  number    = {9},
  year      = {1977},
  pages     = {473-487},
}

@Book{weightedautomata09,
  editor =    {Manfred Droste and Werner Kuich and Heiko Vogler},
  title =        {Handbook of Weighted Automata},
  publisher =    {Springer},
  year =         2009
}


