Quelle  root.bib

@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"
}

@Book{Back1998,
  author =       {Back, R.-J. and Wright, J.},
  title =        {Refinement Calculus: A Systematic Introduction},
  publisher =    {Springer},
  year =         1998}

@InProceedings{Ballarin06,
  author =       {Ballarin, C.},
  title =        {Interpretation of Locales in {Isabelle}: Theories and Proof Contexts},
  booktitle = {Proc. 5th Intl. Conf. on Mathematical Knowledge Management (MKM)},
  year =      2006,
  volume =    4108,
  series =    {LNCS},
  pages =     {31--43},
  publisher = {Springer}}

@Article{Ballarin17,
  author =       {Ballarin, C. and others},
  title =        {The {Isabelle/HOL Algebra Library}},
  journal =      {Isabelle/HOL},
  year =         2017,
  month =     {October},
  note =      {\url{https://isabelle.in.tum.de/library/HOL/HOL-Algebra/document.pdf}}}

@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}
}

@InProceedings{Cavalcanti04,
  author =       {Cavalcanti, A. and Woodcock, J.},
  title =        {A Tutorial Introduction to Designs in Unifying Theories of Programming},
  booktitle =    {Proc. 4th Intl. Conf. on Integrated Formal Methods (IFM)},
  year =         2004,
  volume =       2999,
  series =       {LNCS},
  pages =     {40--66},
  publisher =    {Springer}}

@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"}

@Article{Dijkstra75,
  author =       {Dijkstra, E. W.},
  title =        {Guarded commands, nondeterminacy and formal derivation of programs},
  journal =      {Communications of the ACM},
  year =         1975,
  volume =       18,
  number =       8,
  pages =     {453--457}}

@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}}

@PhdThesis{Foster09,
  author =       {Foster, J.},
  title =        {Bidirectional programming languages},
  school =       {University of Pennsylvania},
  year =         2009}

@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}}

@InProceedings{Foster16a,
  author =       {Foster, S. and Zeyda, F. and Woodcock, J.},
  title =        {Unifying heterogeneous state-spaces with lenses},
  booktitle =    {Proc. 13th Intl. Conf. on Theoretical Aspects of Computing (ICTAC)},
  year =         2016,
  volume =    9965,
  series =       {LNCS},
  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}}

@InProceedings{Foster18a,
  author =       {Foster, S. and Ye, K. and Cavalcanti, A. and Woodcock, J.},
  title =        {Calculational Verification of Reactive Programs with Reactive Relations and {Kleene} Algebra},
  booktitle =    {Proc. 17th Intl. Conf. on Relational and Algebraic Methods in Computer Science (RAMICS)},
  year =      2018,
  volume =    11194,
  series =    {LNCS},
  month =     {October},
  publisher = {Springer}}

@InProceedings{Foster18b,
  author =       {Foster, S. and Baxter, J. and Cavalcanti, A. and Miyazawa, A. and Woodcock, J.},
  title =        {Automating Verification of State Machines with Reactive Designs and {Isabelle/UTP}},
  booktitle = {Proc. 15th. Intl. Conf. on Formal Aspects of Component Software},
  year =      2018,
  volume =    11222,
  series =    {LNCS},
  month =     {October},
  publisher = {Springer}}

@InCollection{Harel1984-DynamicLogic,
  author =       {Harel, D.},
  title =        {Dynamic logic},
  booktitle =    {Handbook of Philosophical Logic},
  publisher = {Springer},
  year =      1984,
  volume =    165,
  series =    {SYLI},
  pages =     {497--604}}

@Article{Hehner1984-PredicativeProgramming,
  author =       {Hehner, E. C. R.},
  title =        {Predicative Programming},
  journal =      {Communications of the ACM},
  year =         1984,
  volume =    27,
  number =    2,
  pages =     {134--151}}

@Article{Hehner1988,
  author =       {Hehner, E. C. R. and Malton, A. J.},
  title =        {Termination Conventions and Comparative Semantics},
  journal =      {Acta Informatica},
  year =         1988,
  volume =    25}

@Article{Hehner1990,
  author =       {Hehner, E. C. R.},
  title =        {A practical theory of programming},
  journal =      {Science of Computer Programming},
  year =         1990,
  volume =    14,
  pages =     {133--158}}

@Book{Hehner93,
  Title                    = {A Practical Theory of Programming},
  Author                   = {E. C. R. Hehner},
  Publisher                = {Springer},
  Year                     = {1993}
}

@Article{Hoare1969-Logic,
  author =       {Hoare, C. A. R.},
  title =        {An axiomatic basis for computer programming},
  journal =      {Communications of the ACM},
  year =         1969,
  volume =    12,
  number =    10,
  pages =     {576--580},
  month =     {October}}

@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}
}

@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}
}

@article{Optics-AFP,
  author  = {Simon Foster and Frank Zeyda},
  title   = {Optics},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2017,
  note    = {\url{http://isa-afp.org/entries/Optics.html},
            Formal proof development},
  ISSN    = {2150-914x},
}