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 Královič, Paweł Urzyczyn, eds.: Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 4162, pp. 447–458, Springer, 2006.
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 Kr\'alovi\v{c} and Pawe\l Urzyczyn},
booktitle = {Mathematical Foundations of Computer Science},
publisher = {Springer},
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},
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.
},
}