@article{ArmstrongGS15,
  author    = {Alasdair Armstrong and
               Victor B. F. Gomes and
               Georg Struth},
  title     = {Building program construction and verification tools from algebraic
               principles},
  journal   = {Formal Aspects of Computing},
  volume    = {28},
  number    = {2},
  pages     = {265--293},
  year      = {2016},
}

@inproceedings{ArmstrongS12,
  author    = {Alasdair Armstrong and
               Georg Struth},
  editor    = {Wolfram Kahl and
               Timothy G. Griffin},
  title     = {Automated Reasoning in Higher-Order Regular Algebra},
  booktitle = {{RAMiCS} 2012},
  series    = {LNCS},
  volume    = {7560},
  pages     = {66--81},
  publisher = {Springer},
  year      = {2012}
}

@article{ArmstrongSW14,
  author    = {Alasdair Armstrong and
               Georg Struth and
               Tjark Weber},
  title     = {Programming and automating mathematics in the {T}arski-{K}leene hierarchy},
  journal   = {J. Logical and Algebraic Methods in Programming},
  volume    = {83},
  number    = {2},
  pages     = {87--102},
  year      = {2014},
}

@book{BackW98,
  author    = {Ralph{-}Johan Back and
               Joakim von Wright},
  title     = {Refinement Calculus - {A} Systematic Introduction},
  publisher = {Springer},
  year      = {1998}
}

@Book{Conway,
	author		= {Conway, J. H.},
	title		= {Regular Algebra and Finite Machines},
	publisher	= {Chapman and Hall},
	year		= 1971
}

@article{DesharnaisMS06,
  author    = {Jules Desharnais and
               Bernhard M{\"{o}}ller and
               Georg Struth},
  title     = {Kleene algebra with domain},
  journal   = {{ACM} Transactions on Computational Logic},
  volume    = {7},
  number    = {4},
  pages     = {798--833},
  year      = {2006}
}

@article{DesharnaisMS11,
  author    = {Jules Desharnais and
               Bernhard M{\"{o}}ller and
               Georg Struth},
  title     = {Algebraic Notions of Termination},
  journal   = {Logical Methods in Computer Science},
  volume    = {7},
  number    = {1},
  year      = {2011},

}

@article{DesharnaisS11,
  author    = {Jules Desharnais and
               Georg Struth},
  title     = {Internal axioms for domain semirings},
  journal   = {Science of Computer Programming},
  volume    = {76},
  number    = {3},
  pages     = {181--203},
  year      = {2011},
}

@inproceedings{DongolGS15,
  author    = {Brijesh Dongol and
               Victor B. F. Gomes and
               Georg Struth},
  title     = {A Program Construction and Verification Tool for Separation Logic},
  booktitle = {{MPC} 2015},
  pages     = {137--158},
  year      = {2015},
  editor    = {Ralf Hinze and
               Janis Voigtl{\"{a}}nder},

  series    = {LNCS},
  volume    = {9129},
  publisher = {Springer},
}

@InCollection{GordonC10,
  author = 	 {Gordon, M. and Collavizza, H.},
  title = 	 {Forward with {H}oare},
  booktitle = 	 {Reflections on the Work of C.A.R. Hoare},
  publisher = {Springer},
  year = 	 2010,
  editor = 	 {Roscoe, A. W. and Jones, C. B. and Wood, K. W.},
  pages = 	 {101--121}}

@book{HarelKT00,
  author    = {David Harel and
               Dexter Kozen and
               Jerzy Tiuryn},
  title     = {Dynamic Logic},
  publisher = {MIT Press},
  year      = {2000}
}

@article{Hollenberg97,
  author    = {Marco Hollenberg},
  title     = {An Equational Axiomatization of Dynamic Negation and Relational Composition},
  journal   = {Journal of Logic, Language and Information},
  volume    = {6},
  number    = {4},
  pages     = {381--401},
  year      = {1997},
}

@Article{JonssonT51,
  author = 	 {J\'onsson, B. and Tarski, A.},
  title = 	 {Boolean Algebras with Operators, Part {I}},
  journal = 	 {Americal Journal of Mathematics},
  year = 	 1951,
  volume = 	 73,
  number = 	 4,
  pages = 	 {207-215}}

@article{Kozen00,
  author    = {Kozen, D.},
  title     = {On {H}oare logic and {K}leene algebra with tests},
  journal   = {ACM TOCL},
  volume    = 1,
  number    = 1,
  year      = 2000,
  pages     = {60--76},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{KozenP00,
  author    = {Dexter Kozen and
               Maria{-}Christina Patron},
  editor    = {John W. Lloyd and al},
  title     = {Certification of Compiler Optimizations Using {K}leene Algebra with
               Tests},
  booktitle = {{CL} 2000}, 
  series    = {LNCS},
  volume    = {1861},
  pages     = {568--582},
  publisher = {Springer},
  year      = {2000}
}

@article{MatichukMW16,
  author    = {Daniel Matichuk and
               Toby C. Murray and
               Makarius Wenzel},
  title     = {Eisbach: {A} Proof Method Language for {I}sabelle},
  journal   = {J. Automated Reasoning},
  volume    = {56},
  number    = {3},
  pages     = {261--282},
  year      = {2016},
}

@inproceedings{MengPK07,
  author    = {Jia Meng and
               Lawrence C. Paulson and
               Gerwin Klein},
  title     = {A Termination Checker for {I}sabelle {H}oare Logic},
  booktitle = {International Verification Workshop},
  year      = 2007,
  url       = {http://ceur-ws.org/Vol-259/paper10.pdf},
}

@article{MollerS06,
  author    = {Bernhard M{\"{o}}ller and
               Georg Struth},
  title     = {Algebras of modal operators and partial correctness},
  journal   = {Theoretical Computer Science},
  volume    = {351},
  number    = {2},
  pages     = {221--239},
  year      = {2006},
}

@book{Morgan94,
  author    = {Morgan, C.},
  title     = {Programming from specifications, 2nd Edition},
  publisher = {Prentice Hall},
  year      = {1994}
}


@inproceedings{Nemeti81,
  author    = {Istv{\'{a}}n N{\'{e}}meti},
  title     = {Dynamic Algebras of Programs},
  booktitle = {FCT'81},
  pages     = {281--290},
  year      = {1981},
  editor    = {Ferenc G{\'{e}}cseg},
  series    = {LNCS},
  volume    = {117},
  publisher = {Springer},
}

@book{NipkowK14,
  author    = {Tobias Nipkow and
               Gerwin Klein},
  title     = {Concrete Semantics---With {I}sabelle/{HOL}},
  publisher = {Springer},
  year      = {2014}
}

@book{NipkowPW02,
  author    = {Nipkow, T. and
               Paulson, L. C. and
               Wenzel, M.},
  title     = {Isabelle/HOL - A Proof Assistant for Higher-Order Logic},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2283},
  year      = {2002}
}

@Book{Platzer,
  author = 	 {Andr\'e Platzer},
  title = 	 {Logical Analysis of Hybrid Systems},
  publisher = 	 {Springer},
  year = 	 2010}



@inproceedings{Pratt88,
  author    = {Vaughan R. Pratt},
  title     = {Dynamic algebras as a well-behaved fragment of relation algebras},
  booktitle = {Algebraic Logic and Universal Algebra in Computer Science},
  pages     = {77--110},
  editor    = {Clifford Bergman and
               Roger D. Maddux and
               Don Pigozzi},
  series    = {LNCS},
  volume    = {425},
  publisher = {Springer},
  year      = {1990},
 
}

@article{Struth12,
  author    = {Georg Struth},
  title     = {Left omega algebras and regular equations},
  journal   = {J. Logic and Algebraic Programming},
  volume    = {81},
  number    = {6},
  pages     = {705--717},
  year      = {2012},
}

@article{Struth16,
  author    = {Georg Struth},
  title     = {On the expressive power of {K}leene algebra with domain},
  journal   = {Information Processing Letters},
  volume    = {116},
  number    = {4},
  pages     = {284--288},
  year      = {2016},

}

@article{afp:ka,
  author    = {Alasdair Armstrong and
               Georg Struth and
               Tjark Weber},
  title     = {Kleene Algebra},
  journal   = {Archive of Formal Proofs},
  year      = {2013}
}

@article{afp:kad,
  author    = {Victor B. F. Gomes and
               Walter Guttman and
               Peter H\"ofner and
               Georg Struth and
               Tjark Weber},
  title     = {Kleene Algebra with domain},
  journal   = {Archive of Formal Proofs},
  year      = {2016}
}

@article{afp:kat,
  author    = {Alasdair Armstrong and
               Victor B. F. Gomes and
               Georg Struth},
  title     = {Kleene Algebra with Tests and Demonic Refinement Algebras},
  journal   = {Archive of Formal Proofs},
  year      = {2014}
}

@phdthesis{Gomes15,
  title={Algebraic Principles for Program Correctness Tools in {I}sabelle/{HOL}},
  author={Victor B. F. Gomes},
  year={2015},
  school={University of Sheffield}
}
