%0 Conference Paper %1 GoncharovEA06 %A Goncharov, Sergey %A Schröder, Lutz %A Mossakowski, Till %B Mathematical Foundations of Computer Science %D 2006 %E Kralovic, Rastislav %E Urzyczyn, Pawel %I Springer; Berlin; http://www.springer.de %K completeness effects evaluation logic monads side %P 447-458 %T Completeness of Global Evaluation Logic %U http://dx.doi.org/10.1007/11821069_39 %V 4162 %X 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.

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