@STRING{cacm="Communications of the ACM"}
@STRING{csur="{ACM} Computing Surveys"}
@STRING{fac="Formal Aspects of Computing"}
@STRING{iandc="Information and Computation"}
@STRING{ipl="Information Processing Letters"}
@STRING{jar="Journal of Automated Reasoning"}
@STRING{lmcs="Logical Methods in Computer Science"}
@STRING{lncs="LNCS"}
@STRING{scp="Science of Computer Programming"}
@STRING{tcs="Theoretical Computer Science"}
@STRING{tocl="{ACM} Transactions on Computational Logic"}

@inproceedings{Abadi:1990,
  author       = {M. Abadi},
  title        = {An Axiomatization of Lamport's Temporal Logic of Actions},
  booktitle    = {{CONCUR} '90},
  series       = lncs,
  volume       = 458,
  pages        = {57--69},
  publisher    = {Springer},
  year         = 1990,
  doi          = {10.1007/BFB0039051},
}

@inproceedings{AbadiPlotkin:1991,
  author    = {M. Abadi and
               G. D. Plotkin},
  title     = {A Logical View of Composition and Refinement},
  booktitle = {POPL'1991},
  pages     = {323--332},
  publisher = {{ACM} Press},
  year      = 1991,
  doi       = {10.1145/99583.99626},
}

@article{AbadiPlotkin:1993,
  author    = {M. Abadi and
               G. D. Plotkin},
  title     = {A Logical View of Composition},
  journal   = tcs,
  volume    = 114,
  number    = 1,
  pages     = {3--30},
  year      = 1993,
  doi       = {10.1016/0304-3975(93)90151-I},
}

@inproceedings{AbadiMerz:1995,
  author    = {M. Abadi and S. Merz},
  title     = {An Abstract Account of Composition},
  booktitle = {MFCS'95},
  series    = lncs,
  volume    = 969,
  pages     = {499--508},
  publisher = {Springer},
  year      = 1995,
  doi       = {10.1007/3-540-60246-1_155},
}

@InCollection{AbadiMerz:1996,
  author    = {M. Abadi and S. Merz},
  title     = {On {TLA} as a logic},
  pages     = {235--271},
  booktitle = {Proceedings of the {NATO} Advanced Study Institute on Deductive Program
               Design, Marktoberdorf, Germany},
  year      = 1996,
  editor    = {Manfred Broy},
  publisher =    {IOS Press},
  isbn         = {3-540-60947-4},
}

@article{AlpernSchneider:1985,
  author    = {B. Alpern and
               F. B. Schneider},
  title     = {Defining Liveness},
  journal   = ipl,
  volume    = 21,
  number    = 4,
  pages     = {181--185},
  year      = 1985,
  doi       = {10.1016/0020-0190(85)90056-0},
}

@article{AlpernDemersSchneider:1986,
  author    = {B. Alpern and
               A. J. Demers and
               F. B. Schneider},
  title     = {Safety Without Stuttering},
  journal   = ipl,
  volume    = 23,
  number    = 4,
  pages     = {177--180},
  year      = 1986,
  doi       = {10.1016/0020-0190(86)90132-8},
}

@TechReport{Schneider:1987,
  author =       {F. B. Schneider},
  title =        {Decomposing Properties into Safety and Liveness using Predicate Logic},
  institution =  {Department of Computer Science, Cornell University},
  year =         1987,
  number =       {87-874},
  month =        oct
}

@article{Emerson:1983,
  author       = {Emerson, E. A.},
  title        = {Alternative Semantics for Temporal Logics},
  journal      = tcs,
  volume       = 26,
  pages        = {121--130},
  year         = 1983,
  doi          = {10.1016/0304-3975(83)90082-8},
}

@article{Brookes:1996,
  author    = {Brookes, S. D.},
  title     = {Full Abstraction for a Shared-Variable Parallel Language},
  journal   = iandc,
  volume    = 127,
  number    = 2,
  pages     = {145--163},
  year      = 1996,
  doi       = {10.1006/inco.1996.0056},
}

@inproceedings{Dingel:1996,
  author    = {J. Dingel},
  title     = {Modular Verification for Shared-Variable Concurrent Programs},
  booktitle = {{CONCUR} '96},
  pages     = {703--718},
  series    = lncs,
  volume    = 1119,
  publisher = {Springer},
  year      = 1996,
  doi       = {10.1007/3-540-61604-7_85},
}

@PhDThesis{Dingel:2000,
  author    = {J. Dingel},
  title     = {Systematic parallel programming},
  school    = {Carnegie Mellon University},
  year      = 2000,
  month     = may,
  note      = {CMU Tech Report CS-99-172},
}

@article{Dingel:2002,
  author    = {J. Dingel},
  title     = {A Refinement Calculus for Shared-Variable Parallel and Distributed
               Programming},
  journal   = fac,
  volume    = 14,
  number    = 2,
  pages     = {123--197},
  year      = 2002,
  doi       = {10.1007/s001650200032},
}

@book{ChandyMisra:1989,
  author    = {Chandy, K. M. and Misra, J.},
  title     = {Parallel program design - a foundation},
  publisher = {Addison-Wesley},
  year      = 1989,
  isbn      = {978-0-201-05866-6},
}

@article{XudeRoeverHe:1997,
  author    = {Xu, Q. and
               de Roever, W.-P. and
               He, J.},
  title     = {The Rely-Guarantee Method for Verifying Shared Variable Concurrent
               Programs},
  journal   = fac,
  volume    = 9,
  number    = 2,
  pages     = {149--174},
  year      = 1997,
  doi       = {10.1007/BF01211617},
}

@book{deRoeverEngelhardt:1998,
  author = {de Roever, W.-P. and Engelhardt, K.},
  title = {Data Refinement: Model-Oriented Proof Methods and their Comparison},
  publisher = {Cambridge University Press},
  pages = 430,
  year = 1998,
  annote = {With the assistance of J. Coenen, K.-H. Buth, P. Gardiner, Y. Lakhnech, and F. Stomp}
}

@book{deRoeverEtAl:2001,
  author    = {de Roever, W.-P. and
               de Boer, F. S. and
               U. Hannemann and
               J. Hooman and
               Y. Lakhnech and
               M. Poel and
               J. Zwiers},
  title     = {Concurrency Verification: Introduction to Compositional and Noncompositional Methods},
  publisher = {Cambridge University Press},
  series    = {Cambridge Tracts in Theoretical Computer Science},
  volume    = 54,
  year      = 2001,
  isbn      = {0-521-80608-9},
}

@article{Kindler:1994,
  author =       {E. Kindler},
  title =        {Safety and liveness properties: A survey},
  journal =      {Bulletin of the European Association for Theoretical Computer Science},
  year =         1994,
  volume =    53,
  number =    30,
  pages =     {268--272},
  month =     6,
}

@article{Kozen:1994,
  author    = {D. Kozen},
  title     = {A Completeness Theorem for Kleene Algebras and the Algebra of Regular
               Events},
  journal   = iandc,
  volume    = 110,
  number    = 2,
  pages     = {366--390},
  year      = 1994,
  doi       = {10.1006/inco.1994.1037},
}

@inproceedings{Maier:2001,
  author    = {P. Maier},
  title     = {A Set-Theoretic Framework for Assume-Guarantee Reasoning},
  booktitle = {ICALP'2001},
  pages     = {821--834},
  series    = lncs,
  volume    = 2076,
  publisher = {Springer},
  year      = 2001,
  doi       = {10.1007/3-540-48224-5_67},
}

@inproceedings{Maier:2004,
  author       = {P. Maier},
  title        = {Intuitionistic {LTL} and a New Characterization of Safety and Liveness},
  booktitle    = {{CSL} 2004},
  series       = lncs,
  volume       = 3210,
  pages        = {295--309},
  publisher    = {Springer},
  year         = 2004,
  doi          = {10.1007/978-3-540-30124-0\_24},
}

@incollection{Hoare:1980,
  author    = {Hoare, C. A. R.},
  title     = {A Model for Communicating Sequential Processes},
  booktitle = {On the Construction of Programs},
  pages     = {229--254},
  year      = 1980,
  publisher = {Cambridge University Press},
  isbn      = {978-0-521-23090-2},
}

@book{Hoare:1985,
  author    = {Hoare, C. A. R.},
  title     = {Communicating Sequential Processes},
  publisher = {Prentice-Hall},
  year      = 1985,
  isbn      = {0-13-153271-5},
}

@article{HoareHe:1987,
  author    = {Hoare, C. A. R. and He, J.},
  title     = {The Weakest Prespecification},
  journal   = ipl,
  volume    = 24,
  number    = 2,
  pages     = {127--132},
  year      = 1987,
  doi       = {10.1016/0020-0190(87)90106-2},
  note      = {Oxford Technical Monograph PRG-44}
}

@article{HoareHeSanders:1987,
  author    = {Hoare, C. A. R. and He, J. and Sanders, J. W.},
  title     = {Prespecification in Data Refinement},
  journal   = ipl,
  volume    = 25,
  number    = 2,
  pages     = {71--76},
  year      = 1987,
  doi       = {10.1016/0020-0190(87)90224-9},
}

@inproceedings{HoareHeSampaio:2000,
  author       = {C. A. R. Hoare and
                  J. He and
                  A. Sampaio},
  editor       = {G. D. Plotkin and
                  C. Stirling and
                  M. Tofte},
  title        = {Algebraic derivation of an operational semantics},
  booktitle    = {Proof, Language, and Interaction, Essays in Honour of Robin Milner},
  pages        = {77--98},
  publisher    = {The {MIT} Press},
  year         = 2000,
}

@article{HoareMoellerStruthWehrman:2011,
  author    = {T. Hoare and
               B. M{\"{o}}ller and
               G. Struth and
               I. Wehrman},
  title     = {Concurrent Kleene Algebra and its Foundations},
  journal   = {Journal of Logic and Algebraic Programming},
  volume    = 80,
  number    = 6,
  pages     = {266--296},
  year      = 2011,
  doi       = {10.1016/j.jlap.2011.04.005},
}

@inproceedings{Park:1980,
  author    = {D. Park},
  title     = {On the Semantics of Fair Parallelism},
  booktitle = {Abstract Software Specifications, 1979 Copenhagen Winter School, January
               22 - February 2, 1979, Proceedings},
  pages     = {504--526},
  series    = lncs,
  volume    = 86,
  publisher = {Springer},
  year      = 1980,
  doi       = {10.1007/3-540-10007-5_47},
}

@book{Roscoe:2010,
  author    = {A. W. Roscoe},
  title     = {Understanding Concurrent Systems},
  series    = {Texts in Computer Science},
  publisher = {Springer},
  year      = 2010,
  doi       = {10.1007/978-1-84882-258-0},
  isbn      = {978-1-84882-257-3},
}

@article{Winskel:1985,
  author    = {G. Winskel},
  title     = {On Powerdomains and Modality},
  journal   = tcs,
  volume    = 36,
  pages     = {127--137},
  year      = 1985,
  doi       = {10.1016/0304-3975(85)90037-4},
}

@article{PfaltzSlapal:2013,
  author =       {Pfaltz, J. L. and Šlapal, J.},
  title =        {Transformations of discrete closure systems},
  journal =      {Acta Mathematica Hungarica},
  year =         2013,
  volume =    138,
  number =    4,
  pages =     {386--405},
  doi = {10.1007/s10474-012-0262-z}
}

@inproceedings{deBoerEtAl:1991,
  author    = {de Boer, F. S. and
               Kok, J. N. and
               Palamidessi, C.  and
               Rutten, J. J. M. M.},
  title     = {The Failure of Failures in a Paradigm for Asynchronous Communication},
  booktitle = {{CONCUR} '91},
  series    = lncs,
  volume    = 527,
  pages     = {111--126},
  publisher = {Springer},
  year      = 1991,
  doi       = {10.1007/3-540-54430-5_84},
}

@book{Reynolds:1998,
  author    = {J. C. Reynolds},
  title     = {Theories of programming languages},
  publisher = {Cambridge University Press},
  year      = 1998,
  isbn      = {978-0-521-59414-1},
}

@article{Stirling:1988,
  author    = {C. Stirling},
  title     = {A Generalization of {Owicki-Gries}'s {Hoare} Logic for a Concurrent while
               Language},
  journal   = tcs,
  volume    = 58,
  pages     = {347--359},
  year      = 1988,
  doi       = {10.1016/0304-3975(88)90033-3}
}

@inproceedings{XuHe:1991,
  author    = "Xu, Q. and He, J.",
  editor    = "Morris, Joseph M. and Shaw, Roger C.",
  title     = "A Theory of State-based Parallel Programming: Part 1",
  booktitle = "4th Refinement Workshop",
  year      = 1991,
  publisher = {Springer},
  pages     = "326--359"
}

@inproceedings{XuHe:1994,
  author    = {Q. Xu and J. He},
  editor    = {David Till},
  title     = {Laws of Parallel Programming with Shared Variables},
  booktitle = {6th Refinement Workshop, Proceedings of the 6th Refinement Workshop,
               organised by BCS-FACS, London, UK, 5-7 January 1994},
  series    = {Workshops in Computing},
  pages     = {205--216},
  publisher = {Springer},
  year      = 1994,
  doi       = {10.1007/978-1-4471-3240-0_11}
}

@inproceedings{Abrahamson:1979,
  author    = {K. R. Abrahamson},
  editor    = {G. Kahn},
  title     = {Modal Logic of Concurrent Nondeterministic Programs},
  booktitle = {Semantics of Concurrent Computation, Proceedings of the International
               Symposium, Evian, France, July 2-4, 1979},
  series    = lncs,
  volume    = 70,
  pages     = {21--33},
  publisher = {Springer},
  year      = 1979,
  doi       = {10.1007/BFb0022461},
}

@book{Milner:1989,
 author     = {R. Milner},
 title      = {Communication and Concurrency},
 year       = {1989},
 publisher  = {Prentice-Hall},
}

@inproceedings{DinsdaleYoungEtAl:2013,
  author    = {Dinsdale{-}Young, T. and
               L. Birkedal and
               P. Gardner and
               M. J. Parkinson and
               H. Yang},
  editor    = {R. Giacobazzi and
               R. Cousot},
  title     = {Views: compositional reasoning for concurrent programs},
  booktitle = {{POPL} 2013},
  pages     = {287--300},
  publisher = {{ACM}},
  year      = 2013,
  doi       = {10.1145/2429069.2429104},
}

@inproceedings{vanStaden:2014,
  author    = {van Staden, S.},
  title     = {Constructing the Views Framework},
  booktitle = {{UTP} 2014},
  series    = lncs,
  volume    = 8963,
  pages     = {62--83},
  publisher = {Springer},
  year      = 2014,
  doi       = {10.1007/978-3-319-14806-9_4},
}

@inproceedings{vanStaden:2015,
  author    = {van Staden, S.},
  title     = {On Rely-Guarantee Reasoning},
  booktitle = {{MPC} 2015},
  series    = lncs,
  volume    = 9129,
  pages     = {30--49},
  publisher = {Springer},
  year      = 2015,
  doi       = {10.1007/978-3-319-19797-5_2},
}

@inproceedings{ArmstrongGomesStruth:2014,
  author    = {Armstrong, A. and
               Gomes, V. B. F. and
               Struth, G.},
  title     = {Algebraic Principles for Rely-Guarantee Style Concurrency Verification
               Tools},
  booktitle = {{FM} 2014},
  series    = lncs,
  volume    = 8442,
  pages     = {78--93},
  publisher = {Springer},
  year      = 2014,
  doi       = {10.1007/978-3-319-06410-9_6},
}

@article{Hayes:2016,
  author    = {I. J. Hayes},
  title     = {Generalised rely-guarantee concurrency: an algebraic foundation},
  journal   = fac,
  volume    = 28,
  number    = 6,
  pages     = {1057--1078},
  year      = 2016,
  doi       = {10.1007/s00165-016-0384-0},
}

@book{DaveyPriestley:2002,
  author    = {Davey, B. A. and
               Priestley, H. A.},
  title     = {Introduction to Lattices and Order, Second Edition},
  publisher = {Cambridge University Press},
  year      = 2002,
  doi       = {10.1017/CBO9780511809088},
  isbn      = {978-0-521-78451-1},
}

@book{Vickers:1989,
  author = {Vickers, S.},
  title = {Topology via Logic},
  year = 1989,
  publisher = {Cambridge University Press},
  isbn = 0521360625,
}

@book{Esakia:2019,
  author = {Esakia, L. and Bezhanishvili, G. and Holliday, W. H. and Evseev, A.},
  title = {Heyting Algebras: Duality Theory},
  year = 2019,
  publisher = {Springer},
  edition = {1st},
  isbn = 3030120953,
}

@book{vanDalen:2004,
  author    = {van Dalen, D.},
  title     = {Logic and structure {(4.} ed.)},
  series    = {Universitext},
  publisher = {Springer},
  year      = 2004,
  isbn      = {978-3-540-57839-0},
}

@inproceedings{PrensaNieto:2003,
  author    = {Prensa Nieto, L.},
  title     = {The Rely-Guarantee Method in Isabelle/HOL},
  booktitle = {{ESOP} 2003},
  series    = lncs,
  volume    = 2618,
  pages     = {348--362},
  publisher = {Springer},
  year      = 2003,
  doi       = {10.1007/3-540-36575-3_24},
}

@inproceedings{WickersonDoddsParkinson:2010,
  author    = {Wickerson, J. and Dodds, M. and Parkinson, M. J.},
  title     = {Explicit Stabilisation for Modular Rely-Guarantee Reasoning},
  booktitle = {{ESOP} 2010},
  series    = lncs,
  volume    = 6012,
  pages     = {610--629},
  publisher = {Springer},
  year      = 2010,
  doi       = {10.1007/978-3-642-11957-6_32},
  url       = {https://johnwickerson.github.io/expstab.thy.html},
  note      = {Extended version in UCAM-CL-TR-774}
}

@article{Jones:1983,
  author       = {C. B. Jones},
  title        = {Tentative Steps Toward a Development Method for Interfering Programs},
  journal      = toplas,
  volume       = 5,
  number       = 4,
  pages        = {596--619},
  year         = 1983,
  doi          = {10.1145/69575.69577},
}

@inproceedings{HayesJones:2017,
  author    = {Hayes, I. J. and Jones, C. B.},
  title     = {A Guide to Rely/Guarantee Thinking},
  booktitle = {{SETSS} 2017},
  series    = lncs,
  volume    = 11174,
  pages     = {1--38},
  publisher = {Springer},
  year      = 2017,
  doi       = {10.1007/978-3-030-02928-9_1},
}

@article{HoareEtAl:1987,
  author    = {C. A. R. Hoare and
               I. J. Hayes and
               J. He and
               C. Morgan and
               A. W. Roscoe and
               J. W. Sanders and
               I. H. S{\o}rensen and
               J. M. Spivey and
               B. Sufrin},
  title     = {Laws of Programming},
  journal   = cacm,
  volume    = 30,
  number    = 8,
  pages     = {672--686},
  year      = 1987,
  doi       = {10.1145/27651.27653},
}

@inproceedings{Feng:2009,
  author    = {X. Feng},
  editor    = {Z. Shao and B. C. Pierce},
  title     = {Local rely-guarantee reasoning},
  booktitle = {{POPL} 2009},
  pages     = {315--327},
  publisher = {{ACM}},
  year      = 2009,
  doi       = {10.1145/1480881.1480922},
  note      = "Also Technical Report TTIC-TR-2008-1"
}

@article{LiangFenFu:2014,
  author    = {H. Liang and
               X. Feng and
               M. Fu},
  title     = {Rely-Guarantee-Based Simulation for Compositional Verification of
               Concurrent Program Transformations},
  journal   = toplas,
  volume    = 36,
  number    = 1,
  pages     = {3:1--3:55},
  year      = 2014,
  doi       = {10.1145/2576235},
}

@article{MisraChandy:1981,
  author    = {Misra, J. and Chandy, K. M.},
  title     = {Proofs of Networks of Processes},
  journal   = {{IEEE} Trans. Software Eng.},
  volume    = 7,
  number    = 4,
  pages     = {417--426},
  year      = 1981,
  doi       = {10.1109/TSE.1981.230844},
}

@inproceedings{Plotkin:2006,
  author    = {G. D. Plotkin},
  title     = {{Hennessy}-{Plotkin}-{Brookes} Revisited},
  booktitle = {{FSTTCS} 2006},
  series    = lncs,
  volume    = 4337,
  pages     = 4,
  publisher = {Springer},
  year      = 2006,
  doi       = {10.1007/11944836_2},
}

@inproceedings{JagadeesanEtAl:2012,
  author    = {R. Jagadeesan and
               G. Petri and
               J. Riely},
  editor    = {Lars Birkedal},
  title     = {Brookes Is Relaxed, Almost!},
  booktitle = {{FOSSACS} 2012},
  series    = lncs,
  volume    = 7213,
  pages     = {180--194},
  publisher = {Springer},
  year      = 2012,
  doi       = {10.1007/978-3-642-28729-9_12},
}

@article{OwickiGries:1976,
  author       = {S. S. Owicki and D. Gries},
  title        = {An Axiomatic Proof Technique for Parallel Programs {I}},
  journal      = {Acta Informatica},
  volume       = 6,
  pages        = {319--340},
  year         = 1976,
  doi          = {10.1007/BF00268134},
}

@article{OwickiLamport:1982,
  author    = {S. S. Owicki and L. Lamport},
  title     = {Proving Liveness Properties of Concurrent Programs},
  journal   = toplas,
  volume    = 4,
  number    = 3,
  pages     = {455--495},
  year      = 1982,
  doi       = {10.1145/357172.357178},
}

@inproceedings{Lamport:1983,
  author    = {L. Lamport},
  editor    = {R. E. A. Mason},
  title     = {What Good is Temporal Logic?},
  booktitle = {Information Processing 83, Proceedings of the {IFIP} 9th World Computer
               Congress, Paris, France, September 19-23, 1983},
  pages     = {657--668},
  publisher = {North-Holland/IFIP},
  year      = 1983,
}

@inproceedings{Lamport:1985,
  author       = {Leslie Lamport},
  title        = {Basic Concepts -- Logical Foundation},
  booktitle    = {Distributed Systems: Methods and Tools for Specification, An Advanced
                  Course, April 3-12, 1984 and April 16-25, 1985, Munich, Germany},
  series       = lncs,
  volume       = 190,
  pages        = {7--43},
  publisher    = {Springer},
  year         = 1985,
  doi          = {10.1007/3-540-15216-4\_12},
  note         = {Formal definition of safety on p27},
}

@article{Lamport:1990,
  author    = {Leslie Lamport},
  title     = {\emph{win} and \emph{sin}: Predicate Transformers for Concurrency},
  journal   = toplas,
  volume    = 12,
  number    = 3,
  pages     = {396--428},
  year      = 1990,
}

@article{AbadiLamport:1991,
  author    = {M. Abadi and L. Lamport},
  title     = {The Existence of Refinement Mappings},
  journal   = tcs,
  volume    = 82,
  number    = 2,
  pages     = {253--284},
  year      = 1991,
  doi       = {10.1016/0304-3975(91)90224-P},
}

@article{Lamport:1994,
  author    = {L. Lamport},
  title     = {The Temporal Logic of Actions},
  journal   = toplas,
  volume    = 16,
  number    = 3,
  pages     = {872--923},
  year      = 1994,
  doi       = {10.1145/177492.177726},
}

@article{AbadiLamport:1995,
  author    = {M. Abadi and
               L. Lamport},
  title     = {Conjoining Specifications},
  journal   = toplas,
  volume    = 17,
  number    = 3,
  pages     = {507--534},
  year      = 1995,
  doi       = {10.1145/203095.201069},
}

@InCollection{Lamport:1999,
  author =       {L. Lamport},
  title =        {Specifying Concurrent Systems in {TLA}\textsuperscript{+}},
  pages =        {183--247},
  booktitle =    {Calculational System Design},
  publisher =    {IOS Press},
  month =        jan,
  year =         2000,
  volume =       173,
  series =       {NATO Science Series, III: Computer and Systems Sciences},
  editor =    {Broy, M. and Steinbrüggen, R.},
  note = {Proceedings of Marktoberdorf 1998},
  isbn = 9789051994599,
}

@book{Lamport:2002,
  author    = {L. Lamport},
  title     = {Specifying Systems, The {TLA}\textsuperscript{+} Language and Tools for Hardware
               and Software Engineers},
  publisher = {Addison-Wesley},
  year      = 2002,
  isbn      = {0-3211-4306-X},
}

@inproceedings{Lamport:1997,
  author    = {L. Lamport},
  editor    = {de Roever, W.-P. and Langmaack, H. and Pnueli, A.},
  title     = {Composition: {A} Way to Make Proofs Harder},
  booktitle = {Compositionality: The Significant Difference ({COMPOS'97})},
  series    = lncs,
  volume    = 1536,
  pages     = {402--423},
  publisher = {Springer},
  year      = 1997,
  doi       = {10.1007/3-540-49213-5_15},
}

@inproceedings{Shankar:1997,
  author    = {N. Shankar},
  editor    = {de Roever, W.-P. and
               Langmaack, H. and
               Pnueli, A.},
  title     = {Lazy Compositional Verification},
  booktitle = {Compositionality: The Significant Difference ({COMPOS'97})},
  series    = lncs,
  volume    = 1536,
  pages     = {541--564},
  publisher = {Springer},
  year      = 1997,
  doi       = {10.1007/3-540-49213-5_21},
}

@inproceedings{MeltonSchmidtStrecker:1985,
  author    = {A. Melton and
               D. A. Schmidt and
               G. E. Strecker},
  title     = {Calois Connections and Computer Science Applications},
  booktitle = {Category Theory and Computer Programming},
  series    = lncs,
  volume    = 240,
  pages     = {299--312},
  publisher = {Springer},
  year      = 1985,
  doi       = {10.1007/3-540-17162-2_130},
}

@article{Foster:2020,
title = "Unifying semantic foundations for automated verification tools in Isabelle/UTP",
journal = scp,
volume = 197,
pages = 102510,
year = 2020,
issn = "0167-6423",
doi = "10.1016/j.scico.2020.102510",
author = "S. Foster and J. Baxter and A. Cavalcanti and J. Woodcock and F. Zeyda",
keywords = "Theorem proving, Lenses, Unifying theories of programming, Hoare logic, Isabelle/HOL",
abstract = "The growing complexity and diversity of models used for engineering dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration requires unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He's Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantics. These can be further applied in the development of verification tools, harnessing Isabelle's proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, algebraic and axiomatic semantics, proof tools for Hoare logic and refinement calculus, and UTP theories to encode computational paradigms."
}

@article{JonssonTsay:1996,
  author    = {Jonsson, B. and Tsay, Y.-K.},
  title     = {Assumption/Guarantee Specifications in Linear-Time Temporal Logic},
  journal   = tcs,
  volume    = 167,
  number    = {1{\&}2},
  pages     = {47--72},
  year      = 1996,
  doi       = {10.1016/0304-3975(96)00069-2},
}

@article{ChiltonEtAl:2014,
  author    = {Chilton, C. and
               Jonsson, B. and
               Kwiatkowska, M. Z.},
  title     = {Compositional assume-guarantee reasoning for input/output component theories},
  journal   = scp,
  volume    = 91,
  pages     = {115--137},
  year      = 2014,
  doi       = {10.1016/j.scico.2013.12.010},
}

@inproceedings{SananEtAl:2017,
  author    = {D. San{\'{a}}n and Y. Zhao and Z. Hou and F. Zhang and A. Tiu and Y. Liu},
  title     = {{CSimpl}: {A} Rely-Guarantee-Based Framework for Verifying Concurrent Programs},
  booktitle = {TACAS},
  pages     = {481--498},
  year      = 2017,
  doi       = {10.1007/978-3-662-54577-5_28},
}

@article{SananEtAl:2021,
  author    = {Sanan, D. and Zhao, Y. and Lin, S.-W. and Yang, L.},
  title     = {CSim2: Compositional Top-down Verification of Concurrent Systems Using Rely-Guarantee},
  journal   = toplas,
  volume    = 43,
  number    = 1,
  year      = 2021,
  doi       = {10.1145/3436808},
}

%   isbn      = {3-540-63406-1},
@book{MuellerOlm:1997,
  author    = {M{\"{u}}ller{-}Olm, M.},
  title     = {Modular Compiler Verification - {A} Refinement-Algebraic Approach
               Advocating Stepwise Abstraction},
  series    = lncs,
  volume    = 1283,
  publisher = {Springer},
  year      = 1997,
  doi       = {10.1007/BFb0027453},
}

%  isbn = {013215871X},
@book{Dijkstra:1976,
 author = {E. W. Dijkstra},
 title = {A  Discipline of Programming},
 year = 1976,
 publisher = {Prentice Hall},
}

@book{GierzEtAl:2003,
  place={Cambridge},
  series={Encyclopedia of Mathematics and its Applications},
  title={Continuous Lattices and Domains},
  doi={10.1017/CBO9780511542725},
  publisher={Cambridge University Press},
  author={Gierz, G. and Hofmann, K. H. and Keimel, K. and Lawson, J. D. and Mislove, M. and Scott, D. S.},
  year=2003,
  collection={Encyclopedia of Mathematics and its Applications}
}

@InBook{Scott:1980,
  author =    {Scott, D. S.},
  title =        {The Kleene Symposium},
  chapter =      {Lambda Calculus: Some Models, Some Philosophy},
  publisher =    {Elsevier},
  year =         1980,
  volume =    101,
  series =    {Studies in Logic and the Foundations of Mathematics},
  pages =     {223-265},
  doi =          {10.1016/S0049-237X(08)71262-X}
}

@article{BackvonWright:2000,
  author    = {Back, R.-J. and von Wright, J.},
  title     = {Encoding, Decoding and Data Refinement},
  journal   = fac,
  volume    = 12,
  number    = 5,
  pages     = {313--349},
  year      = 2000,
  doi       = {10.1007/s001650070008},
}

@phdthesis{Vafeiadis:2008,
  author    = {V. Vafeiadis},
  title     = {Modular fine-grained concurrency verification},
  school    = {University of Cambridge, {UK}},
  year      = 2008,
}

@inproceedings{PavlovicPepperSmith:2010,
  author    = {D. Pavlovic and
               P. Pepper and
               D. R. Smith},
  title     = {Formal Derivation of Concurrent Garbage Collectors},
  booktitle = {{MPC} 2010},
  series    = lncs,
  volume    = 6120,
  pages     = {353--376},
  publisher = {Springer},
  year      = 2010,
  doi       = {10.1007/978-3-642-13321-3_20},
}

@inproceedings{PavlovicPepperSmith:2003,
  author    = {D. Pavlovic and
               P. Pepper and
               D. R. Smith},
  title     = {Colimits for Concurrent Collectors},
  booktitle = {Verification: Theory and Practice, Essays Dedicated to Zohar Manna
               on the Occasion of His 64th Birthday},
  series    = lncs,
  volume    = 2772,
  pages     = {568--597},
  publisher = {Springer},
  year      = 2003,
  doi       = {10.1007/978-3-540-39910-0_25},
}

@article{CaiPaige:1989,
  author    = {J. Cai and
               R. Paige},
  title     = {Program Derivation by Fixed Point Computation},
  journal   = scp,
  volume    = 11,
  number    = 3,
  pages     = {197--261},
  year      = 1989,
  doi       = {10.1016/0167-6423(88)90033-0},
}

@inproceedings{MannaPnueli:1988,
  author    = {Z. Manna and
               A. Pnueli},
  title     = {The anchored version of the temporal framework},
  booktitle = {Linear Time, Branching Time and Partial Order in Logics and Models
               for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands,
               May 30 - June 3, 1988, Proceedings},
  editor    = {de Bakker, J. W. and
               de Roever, W. P. and
               Rozenberg, G.},
  pages     = {201--284},
  year      = 1988,
  doi       = {10.1007/BFb0013024},
  volume    = 354,
  publisher = {Springer},
  series    = lncs,
}

@InCollection{MannaPnueli:1991,
  author =       "Z. Manna and A. Pnueli",
  title =        "Tools and rules for the practicing verifier",
  booktitle =    "CMU Computer Science: A 25th Anniversary Commemorative",
  pages =     "121--156",
  publisher = "ACM Press and Addison-Wesley",
  year =      1991,
  editor =    "R. F. Rashid",
  note = "Also Technical Report STAN-CS-90-1321"
}

@inproceedings{MannaPnueli:2010,
  author    = {Z. Manna and A. Pnueli},
  title     = {Temporal Verification of Reactive Systems: Response},
  booktitle = {Time for Verification, Essays in Memory of Amir Pnueli},
  series    = lncs,
  volume    = 6200,
  publisher = {Springer},
  pages     = {279--361},
  year      = 2010,
  doi       = {10.1007/978-3-642-13754-9\_13},
}

@inproceedings{HawblitzelEtAl:2015,
  author    = {C. Hawblitzel and
               E. Petrank and
               S. Qadeer and
               S. Tasiran},
  title     = {Automated and Modular Refinement Reasoning for Concurrent Programs},
  booktitle = {CAV'2015},
  series    = lncs,
  volume    = 9207,
  pages     = {449--465},
  publisher = {Springer},
  year      = 2015,
  doi       = {10.1007/978-3-319-21668-3_26},
}

@inproceedings{SiegelStomp:1994,
  author    = {M. Siegel and
               F. A. Stomp},
  title     = {Extending the Limits of Sequentially Phased Reasoning},
  booktitle = {FSTTCS`94},
  series    = lncs,
  volume    = 880,
  pages     = {402--413},
  publisher = {Springer},
  year      = 1994,
  doi       = {10.1007/3-540-58715-2_141},
}

@inproceedings{CousotCousot:1979,
  author       = {Patrick Cousot and
                  Radhia Cousot},
  editor       = {Alfred V. Aho and
                  Stephen N. Zilles and
                  Barry K. Rosen},
  title        = {Systematic Design of Program Analysis Frameworks},
  booktitle    = {Conference Record of the Sixth Annual {ACM} Symposium on Principles
                  of Programming Languages, San Antonio, Texas, USA, January 1979},
  pages        = {269--282},
  publisher    = {{ACM} Press},
  year         = 1979,
  doi          = {10.1145/567752.567778},
}

@article{CousotCousot:1992,
  author    = {P. Cousot and
               R. Cousot},
  title     = {Abstract Interpretation Frameworks},
  journal   = {Journal of Logic and Computation},
  volume    = 2,
  number    = 4,
  pages     = {511--547},
  year      = 1992,
  doi       = {10.1093/logcom/2.4.511},
}

@inproceedings{DoligezGonthier:1994,
  author    = {D. Doligez and
               G. Gonthier},
  title     = {Portable, Unobtrusive Garbage Collection for Multiprocessor
               Systems},
  booktitle = {POPL'1994},
  publisher = {ACM Press},
  year      = 1994,
  pages     = {70-83},
  doi       = {10.1145/174675.174673},
}

@article{ZakowskiEtAl:2019,
  author    = {Y. Zakowski and
               D. Cachera and
               D. Demange and
               G. Petri and
               D. Pichardie and
               S. Jagannathan and
               J. Vitek},
  title     = {Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology},
  journal   = jar,
  volume    = 63,
  number    = 2,
  pages     = {489--515},
  year      = 2019,
  doi       = {10.1007/s10817-018-9489-x},
}

@article{JonesYatapanage:2019,
  author    = {C. B. Jones and
               N. Yatapanage},
  title     = {Investigating the limits of rely/guarantee relations based on a concurrent
               garbage collector example},
  journal   = fac,
  volume    = {31},
  number    = {3},
  pages     = {353--374},
  year      = {2019},
  doi       = {10.1007/s00165-019-00482-3},
}

@article{KapoorLodayaReddy:2011,
  author    = {K. Kapoor and
               K. Lodaya and
               U. S. Reddy},
  title     = {Fine-grained Concurrency with Separation Logic},
  journal   = {Journal of Philosophical Logic},
  volume    = 40,
  number    = 5,
  pages     = {583--632},
  year      = 2011,
  doi       = {10.1007/s10992-011-9195-1},
}

% Imperative HOL and thereabouts

%  isbn =        {978-3-540-71065-3},
%  editor =      {O. A. Mohamed and C. Mu{\~n}oz and S. Tahar}
@inproceedings{Bulwahn-et-al:2008:imp_HOL,
  author =      {L. Bulwahn and A. Krauss and F. Haftmann and L. Erk{\"o}k and J. Matthews},
  title =       {Imperative Functional Programming with {Isabelle/HOL}},
  booktitle =   {TPHOLs'08},
  year =        2008,
  pages =       {352--367},
  publisher =   {Springer},
  series =      lncs,
  volume =      5170,
}

@article{KavanaghBrookes:2019,
  author    = {R. Kavanagh and
               S. Brookes},
  title     = {A Denotational Semantics for {SPARC} {TSO}},
  journal   = lmcs,
  volume    = 15,
  number    = 2,
  year      = 2019,
  doi       = {10.23638/LMCS-15(2:10)2019},
}

@inproceedings{ManoliosTrefler:2003,
  author    = {Manolios, P. and Trefler, R. J.},
  editor    = {E. Borowsky and S. Rajsbaum},
  title     = {A lattice-theoretic characterization of safety and liveness},
  booktitle = {{PODC}'2003},
  pages     = {325--333},
  publisher = {{ACM}},
  year      = 2003,
  doi       = {10.1145/872035.872083},
}

@inproceedings{MorrisettFelleisenHarper:1995,
  author    = {J. G. Morrisett and
               M. Felleisen and
               R. Harper},
  title     = {Abstract Models of Memory Management},
  booktitle = {{FPCA} 1995},
  pages     = {66--77},
  publisher = {{ACM}},
  year      = 1995,
  doi       = {10.1145/224164.224182},
  note      = {see also CMU Tech Report CS-96-176},
}

@Book{Ono:2019,
  author    = {H. Ono},
  title     = {Proof Theory and Algebra in Logic},
  publisher = {Springer},
  series    = {Short Textbooks in Logic},
  year      = 2019,
  doi       = {10.1007/978-981-13-7997-0}
}

@Article{Stone:1938,
  author =       {Stone, M. H.},
  title =        {Topological representations of distributive lattices and {Brouwerian} logics},
  journal =      {Časopis pro pěstování matematiky a fysiky},
  year =         1938,
  volume =       67,
  number =       1,
  pages =        {1--25},
  doi = {10.21136/CPMF.1938.124080}
}

@inproceedings{Backhouse:2000,
  author    = {Backhouse, R. C.},
  editor    = {Backhouse, R.C. and
               Crole, R. L. and
               Gibbons, J.},
  title     = {Galois Connections and Fixed Point Calculus},
  booktitle = {Algebraic and Coalgebraic Methods in the Mathematics of Program Construction},
  series    = lncs,
  volume    = 2297,
  pages     = {89--148},
  publisher = {Springer},
  year      = 2000,
  doi       = {10.1007/3-540-47797-7_4},
}

@inproceedings{XuCauCollette:1994,
  author       = {Q. Xu and
                  A. Cau and
                  P. Collette},
  editor       = {B. Jonsson and J. Parrow},
  title        = {On Unifying Assumption-Commitment Style Proof Rules for Concurrency},
  booktitle    = {{CONCUR} '94},
  series       = lncs,
  volume       = 836,
  pages        = {267--282},
  publisher    = {Springer},
  year         = 1994,
  doi          = {10.1007/978-3-540-48654-1\_22},
}

@article{CauCollette:1996,
  author    = {A. Cau and
               P. Collette},
  title     = {Parallel Composition of Assumption-Commitment Specifications: {A}
               Unifying Approach for Shared Variable and Distributed Message Passing
               Concurrency},
  journal   = {Acta Informatica},
  volume    = 33,
  number    = 2,
  pages     = {153--176},
  year      = 1996,
  doi       = {10.1007/s002360050039},
}

@inproceedings{Jackson:1998,
  author    = {P. B. Jackson},
  title     = {Verifying a Garbage Collection Algorithm},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = lncs,
  volume    = {1479},
  year      = 1998,
  pages     = {225-244},
  doi       = {10.1007/BFb0055139},
}

@book{Lynch:1996,
  author    = {N. A. Lynch},
  title     = {Distributed Algorithms},
  publisher = {Morgan Kaufmann},
  year      = 1996,
  isbn      = {1-55860-348-4},
}

@inproceedings{Pratt:1990,
  author    = {V. R. Pratt},
  editor    = {van Eijck, J.},
  title     = {Action Logic and Pure Induction},
  booktitle = {Logics in AI, European Workshop, {JELIA} '90, Amsterdam, The Netherlands,
               September 10-14, 1990, Proceedings},
  series    = lncs,
  volume    = 478,
  pages     = {97--120},
  publisher = {Springer},
  year      = 1990,
  doi       = {10.1007/BFb0018436},
}

@article{Sistla:1994,
  author    = {Sistla, A. P.},
  title     = {Safety, Liveness and Fairness in Temporal Logic},
  journal   = fac,
  volume    = 6,
  number    = 5,
  pages     = {495--512},
  year      = 1994,
  doi       = {10.1007/BF01211865},
}

@book{KroegerMerz:2008,
  author    = {F. Kr{\"{o}}ger and S. Merz},
  title     = {Temporal Logic and State Systems},
  series    = {Texts in Theoretical Computer Science. An {EATCS} Series},
  publisher = {Springer},
  year      = 2008,
  isbn      = {978-3-540-67401-6},
}

@inproceedings{MuellerNipkow:1997,
  author       = {O. M{\"{u}}ller and
                  T. Nipkow},
  title        = {Traces of I/O-Automata in {Isabelle/HOLCF}},
  booktitle    = {{TAPSOFT'97}},
  series       = lncs,
  volume       = 1214,
  pages        = {580--594},
  publisher    = {Springer},
  year         = 1997,
  doi          = {10.1007/BFb0030627},
}

@article{WarfordVegaStaley:2020,
  author    = {Warford, J. S. and
               Vega, D. and
               Staley, S. M.},
  title     = {A Calculational Deductive System for Linear Temporal Logic},
  journal   = csur,
  volume    = 53,
  number    = 3,
  pages     = {53:1--53:38},
  year      = 2020,
  doi       = {10.1145/3387109},
}

@inproceedings{DeGiacomoVardi:2013,
  author       = {De Giacomo, G. and Vardi, M. Y.},
  title        = {Linear Temporal Logic and Linear Dynamic Logic on Finite Traces},
  booktitle    = {{IJCAI'13}},
  pages        = {854--860},
  publisher    = {{IJCAI/AAAI}},
  year         = 2013,
}

@book{Zwiers:1989,
  author    = {J. Zwiers},
  title     = {Compositionality, Concurrency and Partial Correctness - Proof Theories
               for Networks of Processes, and Their Relationship},
  series    = lncs,
  volume    = 321,
  publisher = {Springer},
  year      = 1989,
  doi       = {10.1007/BFb0020836},
  isbn      = {3-540-50845-7},
}

% FIXME how do we do this pleasantly? Want to cite Tarski:1930 in translation in this book
@Book{Woodger:1956,
  author =    {A. Tarski},
  title =        {Logic, Semantics and Metamathematics: Papers from 1923 to 1938},
  publisher =    {Oxford University Press},
  year =         1956,
  note =      {Translated by J. H. Woodger}
}

@Article{Tarski:1930,
  author =       {A. Tarski},
  title =        {{Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. I}},
  journal =      {Monatshefte für Mathematik und Physik},
  year =         1930,
  volume =       37,
  pages =        {361--404},
}

@Article{vanGlabbeekHofner:2019,
  author       = {van Glabbeek, R. and H{\"{o}}fner, P.},
  title        = {Progress, Justness, and Fairness},
  journal      = csur,
  volume       = 52,
  number       = 4,
  pages        = {69:1--69:38},
  year         = 2019,
  doi          = {10.1145/3329125},
}

@TechReport{Rushby:2001,
  author =       {John Rushby},
  title =        {Formal Verification of {McMillan's} Compositional Assume-Guarantee Rule},
  institution =  {Computer Science Laboratory, SRI International},
  year =         2001,
  month =        sep,
}

@article{NamjoshiTrefler:2010,
  author       = {K. S. Namjoshi and R. J. Trefler},
  title        = {On the completeness of compositional reasoning methods},
  journal      = tocl,
  volume       = 11,
  number       = 3,
  pages        = {16:1--16:22},
  year         = 2010,
  doi          = {10.1145/1740582.1740584},
}

%% CImperativeHOL

%% TSO

@inproceedings{OwensSarkarSewell:2009,
  author    = {S. Owens and
               S. Sarkar and
               P. Sewell},
  title     = {A Better x86 Memory Model: {x86-TSO}},
  booktitle = {TPHOLs'2009},
  pages     = {391--407},
  series    = lncs,
  volume    = 5674,
  publisher = {Springer},
  year      = 2009,
  doi       = {10.1007/978-3-642-03359-9_27},
  url       = "https://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.pdf"
}

%% examples

@inproceedings{Attiogbe:2005,
  author    = {J. C. Attiogb{\'{e}}},
  editor    = {Helen Treharne and
               Steve King and
               Martin C. Henson and
               Steve A. Schneider},
  title     = {A Stepwise Development of the Peterson's Mutual Exclusion Algorithm
               Using {B} Abstract Systems},
  booktitle = {{ZB} 2005: Formal Specification and Development in {Z} and B, 4th
               International Conference of {B} and {Z} Users, Guildford, UK, April
               13-15, 2005, Proceedings},
  series    = lncs,
  volume    = 3455,
  pages     = {124--141},
  publisher = {Springer},
  year      = 2005,
  doi       = {10.1007/11415787_8},
}

@article{Peterson:1981,
  author    = {G. L. Peterson},
  title     = {Myths About the Mutual Exclusion Problem},
  journal   = ipl,
  volume    = 12,
  number    = 3,
  pages     = {115--116},
  year      = 1981,
  doi       = {10.1016/0020-0190(81)90106-X},
}

@article{Peterson:1983,
  author    = {G. L. Peterson},
  title     = {A New Solution to Lamport's Concurrent Programming Problem Using Small
               Shared Variables},
  journal   = toplas,
  volume    = 5,
  number    = 1,
  pages     = {56--65},
  year      = 1983,
  doi       = {10.1145/357195.357199},
}

@article{KarpMiller:1969,
  author       = {R. M. Karp and R. E. Miller},
  title        = {Parallel Program Schemata},
  journal      = {Journal of Computer and System Sciences},
  volume       = 3,
  number       = 2,
  pages        = {147--195},
  year         = 1969,
  doi          = {10.1016/S0022-0000(69)80011-5},
}

@article{Rosen:1976,
  author       = {B. K. Rosen},
  title        = {Correctness of Parallel Programs: The Church-Rosser Approach},
  journal      = tcs,
  volume       = 2,
  number       = 2,
  pages        = {183--207},
  year         = 1976,
  doi          = {10.1016/0304-3975(76)90032-3},
}

@book{AptDeBoerOlderog:2009,
  author       = {Apt, K. R. and de Boer, F. S. and Olderog, E.{-}R.},
  title        = {Verification of Sequential and Concurrent Programs},
  series       = {Texts in Computer Science},
  publisher    = {Springer},
  year         = 2009,
  doi          = {10.1007/978-1-84882-745-5},
  isbn         = {978-1-84882-744-8},
}

@inproceedings{Ridge:2007,
  author    = {T. Ridge},
  editor    = {K. Schneider and
               J. Brandt},
  title     = {Operational Reasoning for Concurrent Caml Programs and Weak Memory
               Models},
  booktitle = {TPHOLs 2007},
  series    = lncs,
  volume    = 4732,
  pages     = {278--293},
  publisher = {Springer},
  year      = 2007,
  doi       = {10.1007/978-3-540-74591-4_21},
}

@article{vanderSommenEtAl:1997,
  author    = {van der Sommen, F. W. and
               Feijen, W. H. J. and
               van Gasteren, A. J. M.},
  title     = {Peterson's Mutual Exclusion Algorithm Revisited},
  journal   = scp,
  volume    = 29,
  number    = 3,
  pages     = {327--334},
  year      = 1997,
  doi       = {10.1016/S0167-6423(97)00003-8},
}

@inproceedings{CousineauEtAl:2012,
  author    = {D. Cousineau and
               D. Doligez and
               L. Lamport and
               S. Merz and
               D. Ricketts and
               H. Vanzetto},
  editor    = {D. Giannakopoulou and
               D. M{\'{e}}ry},
  title     = {{TLA} + Proofs},
  booktitle = {{FM} 2012: Formal Methods - 18th International Symposium, Paris, France,
               August 27-31, 2012. Proceedings},
  series    = lncs,
  volume    = 7436,
  pages     = {147--154},
  publisher = {Springer},
  year      = 2012,
  doi       = {10.1007/978-3-642-32759-9_14},
}

@Book{Goldblatt:1992,
  author =    {R. Goldblatt},
  title =        {Logics of Time and Computation},
  publisher =    {Center for the Study of Language and Information, Stanford},
  year =         1992,
  number =    7,
  series =    {CSLI Lecture Notes},
  edition =   2
}
