by Sergey Goncharov, Lutz Schröder and Till Mossakowski
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.
Reference:
Sergey Goncharov, Lutz Schröder and Till Mossakowski: Completeness of Global Evaluation Logic, In Rastislav Kralovic, Pawel Urzyczyn, eds.: Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 4162, pp. 447–458, Springer; Berlin; http://www.springer.de, 2006. [preprint]
Bibtex Entry:
@InProceedings{GoncharovEA06,
author = {Sergey Goncharov and Lutz Schr{\"o}der and Till Mossakowski},
title = {Completeness of Global Evaluation Logic},
year = {2006},
editor = {Rastislav Kralovic and Pawel Urzyczyn},
booktitle = {Mathematical Foundations of Computer Science},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
volume = {4162},
pages = {447-458},
keywords = {side effects monads evaluation logic completeness},
url = {http://dx.doi.org/10.1007/11821069_39},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/GELcompl.pdf"> [preprint] </a>},
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.
},
}