Quelle  root.bib

@InProceedings{Alkassar2008,
author="Alkassar, E. and Hillebrand, M. and Leinenbach, D. and Schirmer, N. and Starostin, A.",
title="The {Verisoft} Approach to Systems Verification",
booktitle="VSTTE 2008",
year="2008",
publisher="Springer",
pages="209--224",
series="LNCS",
volume="5295"
}

@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 von Wright, J.},
  title =        {Refinement Calculus: A Systematic Introduction},
  publisher =    {Springer},
  year =         1998}

@inproceedings{Back2003,
 author = {Back, R.-J. and Preoteasa, V.},
 title = {Reasoning About Recursive Procedures with Parameters},
 booktitle = {Proc. Workshop on Mechanized Reasoning About Languages with Variable Binding},
 series = {MERLIN '03},
 year = {2003},
 location = {Uppsala, Sweden},
 pages = {1--7},
 publisher = {ACM}
} 


@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{Calcagno2007, 
author={Calcagno, C. and O'Hearn, P. and Yang, H.}, 
booktitle={LICS}, 
title={Local Action and Abstract Separation Logic}, 
year={2007}, 
pages={366--378}, 
month={July},
publisher={IEEE}}

@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{Dongol15,
  author    = {Dongol, B. and
               Gomes, V. and
               Struth, G.},
  title     = {A Program Construction and Verification Tool for Separation Logic},
  booktitle = {{MPC} 2015},
  series    = {LNCS},
  volume    = {9129},
  pages     = {137--158},
  publisher = {Springer},
  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{Fischer2015,
author="Fischer, S. and Hu, Z. and Pacheco, H.",
title="A Clear Picture of Lens Laws",
booktitle="MPC 2015",
year="2015",
publisher="Springer",
pages="215--223",
}

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

@article{Foster07,
 author = {Foster, J. and Greenwald, M. and Moore, J. and Pierce, B. and Schmitt, A.},
 title = {Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-update Problem},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {May 2007},
 volume = {29},
 number = {3},
 month = may,
 year = {2007},
 issn = {0164-0925},
 articleno = {17},
 url = {http://doi.acm.org/10.1145/1232420.1232424},
 doi = {10.1145/1232420.1232424},
 acmid = {1232424},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Bidirectional programming, Harmony, XML, lenses, view update problem},
} 

@InProceedings{Foster11,
  Title                    = {Automated Engineering of Relational and Algebraic Methods in {Isabelle/HOL}},
  Author                   = {Foster, S. and Struth, G. and Weber, T.},
  Booktitle                = {RAMICS 2011},
  Year                     = {2011},
  Pages                    = {52--67},
  Publisher                = {Springer},
  Series                   = {LNCS},
  Volume                   = {6663},
  ISBN                     = {978-3-642-21069-3}
}

@InProceedings{Foster14,
  Title                    = {{Isabelle/UTP}: A Mechanised Theory Engineering Framework},
  Author                   = {Foster, S. and Zeyda, F. and Woodcock, J.},
  Booktitle                = {UTP},
  Year                     = {2014},
  Pages                    = {21--41},
  Publisher                = {Springer},
  Series                   = {LNCS},
  Volume                   = {8963}
}

@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{Foster16b,
  author =       {Foster, S. and Thiele, B. and Cavalcanti, A. and Woodcock, J.},
  title =        {Towards a {UTP} semantics for {Modelica}},
  booktitle =    {Proc. 6th Intl. Symp. on Unifying Theories of Programming},
  month =        {June},
  year =         2016,
  series =       {LNCS},
  volume =       {10134},
  publisher =    {Springer}
}

@Article{Foster2020-IsabelleUTP,
  author =       {Foster, S. and Baxter, J. and Cavalcanti, A. and Woodcock, J. and Zeyda, F.},
  title =        {Unifying Semantic Foundations for Automated Verification Tools in {Isabelle/UTP}},
  journal =      {Science of Computer Programming},
  volume =       {197},
  month =        {October},
  year =         {2020}}

@article{Gibbons17,
  title = "Profunctor Optics: Modular Data Accessors",
  author = "Matthew Pickering and Jeremy Gibbons and Nicolas Wu",
  year = "2017",
  journal = "The Art, Science, and Engineering of Programming",
  number = "2",
  publisher = "AOSA",
  url = "http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/poptics.pdf",
  volume = "1",
}

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

@Book{Hoare85,
  Title                    = {{Communicating Sequential Processes}},
  Author                   = {Hoare, T.},
  Publisher                = {Prentice-Hall},
  Year                     = {1985},
  Size                     = {256}
}

@ARTICLE{Hoare87,
  AUTHOR        = "Hoare, T. and Hayes, I. and He, J.
                   and Morgan, C. and Roscoe, A. and Sanders, J.
                   and S{\o}rensen, I. and Spivey, J. and Sufrin, B.",
  TITLE         = "The Laws of Programming",
  JOURNAL       = "Communications of the ACM",
  VOLUME        = "30",
  NUMBER        = "8",
  PAGES         = "672--687",
  MONTH         = "August",
  YEAR          = "1987"}

@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{Hofmann2011,
  Title                    = {Symmetric lenses},
  Author                   = {Hofmann, M. and Pierce, B. and Wagner, D.},
  Booktitle                = {POPL},
  Year                     = {2011},
  Pages                    = {371--384},
  Publisher                = {IEEE}
}

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

@Book{Isabelle,
  Title                    = {{Isabelle/HOL: A Proof Assistant for Higher-Order Logic}},
  Author                   = {Nipkow, T. and Wenzel, M. and Paulson, L. C.},
  Publisher                = {Springer},
  Year                     = {2002},
  Series                   = {LNCS},
  Volume                   = {2283}
}

@inproceedings{Klein2009,
 author = {Klein, G. and others},
 title = {{seL4}: Formal Verification of an {OS} Kernel},
 booktitle = {Proc. 22nd Symp. on Operating Systems Principles (SOSP)},
 year = {2009},
 pages = {207--220},
 publisher = {ACM}
} 

@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{Oliveira&09,
  AUTHOR        = {Oliveira, M. and Cavalcanti, A. and Woodcock, J.},
  TITLE         = "{A UTP semantics for {C}ircus}",
  JOURNAL       = {Formal Aspects of Computing},
  VOLUME        = {21},
  ISSUE         = {1-2},
  YEAR          = {2009},
  PAGES         = {3--32},
  PUBLISHER     = {Springer}}

@inproceedings{Reynolds2002,
 author = {Reynolds, J.},
 title = {Separation Logic: A Logic for Shared Mutable Data Structures},
 booktitle = {LICS 2012},
 year = {2002},
 pages = {55--74},
 publisher = {IEEE Computer Society}
} 


@InProceedings{Schirmer2009,
title = "State Spaces -- The Locale Way ",
series = "ENTCS",
volume = "254",
pages = "161--179",
year = "2009",
booktitle = "SSV 2009",
author = "Schirmer, N. and Wenzel, M."
}

@Article{Tarski41,
  author =       {Tarski, A.},
  title =        {On the calculus of relations},
  journal =      {J. Symbolic Logic},
  year =         1941,
  volume =    6,
  number =    3,
  pages =     {73--89}}

@Book{Tarski71,
  author =    {Henkin, L. and Monk, J. and Tarski, A.},
  title =        {Cylindric Algebras, Part I.},
  publisher =    {North-Holland},
  year =         1971}



@InProceedings{Woodcock2016,
  author =       {Woodcock, J. and Foster, S. and Butterfield, A.},
  title =        {Heterogeneous Semantics and Unifying Theories},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {7th Intl. Symp. on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA)},
  year =         {2016},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTpages =     {},
  OPTmonth =     {},
  OPTaddress =   {},
  OPTorganization = {},
  OPTpublisher = {},
  note =         {To appear},
  OPTannote =    {}
}

@InProceedings{Zeyda16,
  author =       {Zeyda, F. and Foster, S. and Freitas, L.},
  title =        {An Axiomatic Value Model for {Isabelle/UTP}},
  booktitle =    {Proc. 6th Intl. Symp. on Unifying Theories of Programming},
  year =         2016,
  note =         {To appear}}