@inproceedings{GoncharovEA06,
  abstract = {Monads serve the abstract encapsulation of side effects in semantics and
functional programming. Various monad-based specification languages have
been introduced in order to express requirements on generic
side-effecting programs. A basic role is played here by global
evaluation logic, concerned with formulae which may be thought of as
being universally quantified over the state space; this formalism is the
fundament of more advanced logics such as monad-based Hoare logic or
dynamic logic. We prove completeness of global evaluation logic for
models in cartesian categories with a distinguished Heyting algebra
object.
},
  added-at = {2016-08-05T15:59:03.000+0200},
  author = {Goncharov, Sergey and Schr{\"o}der, Lutz and Mossakowski, Till},
  biburl = {https://www.bibsonomy.org/bibtex/213540c05d071935eb38664e3f3f5d4c2/tillmo},
  booktitle = {Mathematical Foundations of Computer Science},
  editor = {Kralovic, Rastislav and Urzyczyn, Pawel},
  interhash = {ed07c3dedd2986e86ea3c1f8b0d5f7d7},
  intrahash = {13540c05d071935eb38664e3f3f5d4c2},
  keywords = {completeness effects evaluation logic monads side},
  pages = {447-458},
  pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/GELcompl.pdf},
  psurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/GELcompl.ps},
  publisher = {Springer; Berlin; http://www.springer.de},
  series = {Lecture Notes in Computer Science},
  status = {Reviewed},
  timestamp = {2016-08-05T15:59:03.000+0200},
  title = {Completeness of Global Evaluation Logic},
  url = {http://dx.doi.org/10.1007/11821069_39},
  volume = 4162,
  year = 2006
}