@InProceedings{Armstrong2012,
  Title                    = {Automated Reasoning in Higher-Order Regular Algebra},
  Author                   = {Armstrong, A. and Struth, G.},
  Booktitle                = {RAMiCS 2012},
  Year                     = {2012},
  Month                    = {September},
  Publisher                = {Springer},
  Series                   = {LNCS},
  Volume                   = {7560}
}

@InProceedings{Armstrong2013,
  Title                    = {Program Analysis and Verification Based on {Kleene Algebra} in {Isabelle/HOL}},
  Author                   = {Armstrong, A. and Struth, G. and Weber, T.},
  Booktitle                = {ITP},
  Year                     = 2013,
  Publisher                = {Springer},
  Series                   = {LNCS},
  Volume                   = 7998
}

@Article{Armstrong2015,
  author="Armstrong, A. and Gomes, V. and Struth, G.",
  title="Building program construction and verification tools from algebraic principles",
  journal="Formal Aspects of Computing",
  year="2015",
  volume="28",
  number="2",
  pages="265--293"
}

@InProceedings{Blanchette2011,
  Title                    = {Automatic Proof and Disproof in {Isabelle/HOL}},
  Author                   = {Blanchette, J. C. and Bulwahn, L. and Nipkow, T.},
  Booktitle                = {FroCoS},
  Year                     = {2011},
  Pages                    = {12--27},
  Publisher                = {Springer},
  Series                   = {LNCS},
  Volume                   = {6989}
}

@INCOLLECTION{Cavalcanti&06,
  KEY           = "Cavalcanti\&06",
  AUTHOR        = {Cavalcanti, A. and Woodcock, J.},
  TITLE         = {A Tutorial Introduction to {CSP} in Unifying Theories of
                   Programming},
  BOOKTITLE     = {Refinement Techniques in Software Engineering},
  SERIES        = {LNCS},
  PUBLISHER     = {Springer},
  ISBN          = {978-3-540-46253-8},
  PAGES         = {220--268},
  VOLUME        = {3167},
  YEAR          = {2006},
  COMMENT       = "BIB PGL"}

@InProceedings{Dongol2015,
  author = {Dongol, B. and Gomes, V. B. F. and Struth, G.},
  title  = {A Program Construction and Verification Tool for Separation Logic},
  booktitle = {Mathematics of Program Construction (MPC)},
  series = {LNCS},
  publisher = {Springer},
  volume = {9129},
  pages = {137--158},
  year = {2015}
}

@InProceedings{Feliachi2010,
  author =       {Feliachi, A. and Gaudel, M.-C. and Wolff, B.},
  title =        {Unifying Theories in {Isabelle/HOL}},
  booktitle    = {UTP 2010},
  pages    =     {188--206},
  year =         2010,
  volume    =    6445,
  series =       {LNCS},
  publisher = {Springer}}

@InProceedings{Feliachi2012,
  author =       {Feliachi, A. and Gaudel, M.-C. and Wolff, B.},
  title =        {{Isabelle/Circus}: a Process Specification and
                  Verification Environment},
  booktitle    = {VSTTE 2012},
  pages    =     {243--260},
  year =         2012,
  volume    =    7152,
  series =       {LNCS},
  publisher = {Springer}}

@InProceedings{Foster14c,
  author =       {Foster, S. and Zeyda, F. and Woodcock, J.},
  title =        {{Isabelle/UTP}: A Mechanised Theory Engineering Framework},
  booktitle = {UTP},
  year =      2014,
  series =    {LNCS 8963},
  pages =     {21--41},
  publisher = {Springer}}

@Article{Foster15,
  author =       {Foster, S. and Struth, G.},
  title =        {On the fine-structure of {Regular Algebra}},
  journal =      {J. Automated Reasoning},
  year =         2015,
  volume =    42,
  number =    2}

@InProceedings{Foster16a,
  author =       {Foster, S. and Zeyda, F. and Woodcock, J.},
  title =        {Unifying heterogeneous state-spaces with lenses},
  booktitle =    {ICTAC},
  year =         2016,
  series =       {LNCS 9965},
  publisher =    {Springer}}

@InProceedings{Foster16b,
  author =       {Foster, S. and Thiele, B. and Cavalcanti, A. and Woodcock, J.},
  title =        {Towards a {UTP} semantics for {Modelica}},
  booktitle =    {UTP},
  year =         2016,
  series =       {LNCS 10134},
  publisher =    {Springer}}

@InProceedings{Foster16c,
  author =       {Zeyda, F. and Foster, S. and Freitas, L.},
  title =        {An axiomatic value model for {Isabelle/UTP}},
  booktitle =    {UTP},
  year =         2016,
  series =       {LNCS 10134},
  publisher =    {Springer}}

@Article{Foster17b,
  author =       {Foster, S. and Cavalcanti, A. and Woodcock, J. and Zeyda, F.},
  title =        {Unifying theories of time with generalised reactive processes},
  journal =      {Accepted for Information Processing Letters},
  year =         2017,
  month =        {Dec},
  note =         {Preprint: \url{https://arxiv.org/abs/1712.10213}}}

@Book{Hoare&98,
  Title                    = {Unifying {Theories} of {Programming}},
  Author                   = {Hoare, T. and He, J.},
  Publisher                = {Prentice-Hall},
  Year                     = {1998},
  ISBN                     = {ISBN-10: 0134587618},
  Comment                  = {NA PGL},
  Key                      = {Hoare\&98}
}

@InProceedings{Huffman13,
  Title                    = {Lifting and Transfer: A Modular Design for Quotients in {Isabelle/HOL}},
  Author                   = {Huffman, B. and Kun\v{c}ar, O.},
  Booktitle                = {CPP},
  Year                     = {2013},
  Pages                    = {131--146},
  Publisher                = {Springer},
  Series                   = {LNCS},
  Volume                   = {8307}
}

@InProceedings{Klein2012,
  Title = {Mechanised Separation Algebra},
  author = {Klein, G. and Kolanski, R. and Boyton, A.},
  booktitle = {Interactive Theorem Proving (ITP)},
  year = {2012},
  publisher = {Springer},
  series = {LNCS},
  volume = {7406},
  pages = {332--337}
} 

@article{kozen1997kleene,
  title={Kleene algebra with tests},
  author={Kozen, D.},
  journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume={19},
  number={3},
  pages={427--443},
  year={1997},
  publisher={ACM}
}

@PHDTHESIS{Oliveira2005-PHD,
AUTHOR = {M. V. M. Oliveira},
TITLE = {{Formal Derivation of State-Rich Reactive Programs using {\sf\textsl{Circus}}}},
SCHOOL = {{Department of Computer Science - University of York}},
YEAR = {2006},
NOTE = {YCST-2006-02},
ADDRESS = {UK},
}

@BOOK{Morgan90a,
  KEY           = "Morgan90",
  AUTHOR        = "Carroll Morgan",
  TITLE         = "Programming from Specifications",
  PUBLISHER     = "Prentice-Hall",
  ADDRESS       = "London, UK",
  YEAR          = "1990",
  SIZE          = "255",
  ANNOTE        = "",
  COMMENT       = "NA PGL (borrowed from ID's library"}

@INPROCEEDINGS{Oliveira07,
  author =       {Oliveira, M. and Cavalcanti, A. and Woodcock, J.},
  title =        {{Unifying theories in ProofPower-Z}},
  booktitle =    {UTP 2006},
  pages =        {123--140},
  year =         {2007},
  volume =       {4010},
  series    =    {LNCS},
  publisher    = {Springer}
}

@BOOK{zrm,
  AUTHOR       = {J.~M.~Spivey},
  TITLE        = {{The Z Notation: A Reference Manual}},
  YEAR         = {1998},
  PUBLISHER    = {Prentice Hall},
  annote       = {Standard Z notation and mathematical toolkit}
}