@inproceedings{fdb5f6e540d84fddafc4e066358040fe,
title = "Completeness of global evaluation logic",
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.",
author = "Sergey Goncharov and Lutz Schr{\"o}der and Till Mossakowski",
year = "2006",
doi = "10.1007/11821069_39",
language = "English",
isbn = "3540377913",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "447--458",
booktitle = "Mathematical Foundations of Computer Science 2006 - 31st International Symposium, MFCS 2006, Proceedings",
note = "31st International Symposium on Mathematical Foundations of Computer Science, MFCS 2006 ; Conference date: 28-08-2006 Through 01-09-2006",
}