@article{AbramskyV93,
  author    = {Abramsky, S. and
               Vickers, S.},
  title     = {Quantales, Observational Logic and Process Semantics},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {3},
  number    = {2},
  pages     = {161--227},
  year      = {1993}
}

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

@article{Jacobs17,
  author    = {Bart Jacobs},
  title     = {A Recipe for State-and-Effect Triangles},
  journal   = {Logical Methods in Computer Science},
  volume    = 13,
  number    = 2,
  year      = 2017,
}

@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{ArmstrongS12,
  author    = {Armstrong, A. and Struth, G.},
  title     = {Automated Reasoning in Higher-Order Regular Algebra},
  booktitle = {RAMiCS 2012},
  pages     = {66--81},
  series    = {LNCS},
  volume    = {7560},
  publisher = {Springer},
  year      = {2012}
}

@article{ArmstrongSW13,
  author    = {Armstrong, A. and
               Struth, G. and
               Weber, T.},
  title     = {Kleene Algebra},
  journal   = {Archive of Formal Proofs},
  year      = 2013
}

@article{ArmstrongGS16,
  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,
}

@Misc{Ballarin,
  author = 	 {Ballarin, Clemens},
  title = 	 {The {I}sabelle/{HOL} Algebra Library},
  howpublished = {\url{https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/index.html}}
}

@article{DongolGHS17,
  author    = {Dongol, B. and
               Gomes, V. B. F. and
               Hayes, I. J. and
               Struth, G.},
  title     = {Partial Semigroups and Convolution Algebras},
  journal   = {Archive of Formal Proofs},
  year    = 2017,
}

@article{DongolHS17,
  author    = {Dongol, B. and
               Hayes, I. J. and
               Struth, G.},
  title     = {Relational Convolution, Generalised Modalities and Incidence Algebras},
  journal   = {CoRR},
  volume    = {abs/1702.04603},
  year      = {2017},
  url       = {http://arxiv.org/abs/1702.04603},
}

@Book{GierzHKLMS80,
  author = 	 {Gierz, G. and Hofmann, K. H. and Lawson, J. D. and Mislove, M and Scott, D. S.},
  title = 	 {A Compendium of Continuous Lattices},
  publisher = 	 {Springer},
  year = 	 1980}

@article{GomesS15,
  author    = {Gomes, Victor B. F. and
               Struth, Georg},
  title     = {Residuated Lattices},
  journal   = {Archive of Formal Proofs},
  year      = {2015}
}

@article{Guttmann16,
  author    = {Guttmann, Walter},
  title     = {Stone Algebras},
  journal   = {Archive of Formal Proofs},
  year      = {2016}
}

@Book{Johnstone82,
  author = 	 {Johnstone, Peter T.},
  title = 	 {Stone Spaces},
  publisher = 	 {Cambridge University Press},
  year = 	 1982}

@Book{Koppelberg89,
  author = 	 {Koppelberg, Sabine},
  editor = 	 {Monk, J. Donald},
  title = 	 {Handbook of Boolean Algebras},
  publisher = 	 {North-Holland},
  year = 	 {1989},
  OPTvolume = 	 {1}
}

@inproceedings{Kuncar016,
  author    = {Kuncar, Ondrej and Popescu, Andrei},
  title     = {From Types to Sets by Local Type Definitions in Higher-Order Logic},
  booktitle = {{ITP} 2016},
  pages     = {200--218},
  series    = {LNCS},
  volume    = {9807},
  publisher = {Springer},
  year      = {2016},
}

@article{Preoteasa11a,
  author    = {Preoteasa, Viorel},
  title     = {Lattice Properties},
  journal   = {Archive of Formal Proofs},
  year      = {2011}
}

@article{Preoteasa11b,
  author    = {Preoteasa, Viorel},
  title     = {Algebra of Monotonic Boolean Transformers},
  journal   = {Archive of Formal Proofs},
  year      = {2011}
}

@Book{Rosenthal90,
  author = 	 {Rosenthal, Kimmo. I.},
  title = 	 {Quantales and their Applications},
  publisher = 	 {Longman Scientific \& Technical},
  year = 	 1990}

@Misc{Wenzel,
  author = 	 {Wenzel, Markus},
  title = 	 {Session {HOL}-{L}attice},
  howpublished = {\url{https://isabelle.in.tum.de/dist/library/HOL/HOL-Lattice/index.html}}}

@article{GomesGHSW16,
  author    = {Victor B. F. Gomes and
               Walter Guttmann and
               Peter H{\"{o}}fner and
               Georg Struth and
               Tjark Weber},
  title     = {Kleene Algebras with Domain},
  journal   = {Archive of Formal Proofs},
  year      = 2016
}

@article{FurusawaS15,
  author    = {Hitoshi Furusawa and
               Georg Struth},
  title     = {Binary Multirelations},
  journal   = {Archive of Formal Proofs},
  year      = 2015,
}

@book{McIverM05,
  author    = {Annabelle McIver and
               Carroll Morgan},
  title     = {Abstraction, Refinement and Proof for Probabilistic Systems},
  publisher = {Springer},
  year      = 2005,
}

@article{GomesS16,
  author    = {Victor B. F. Gomes and
               Georg Struth},
  title     = {Program Construction and Verification Components Based on Kleene Algebra},
  journal   = {Archive of Formal Proofs},
  year      = 2016,
}

