| Publication type: |
Article in Proceedings |
| Author: |
Sergey Goncharov, Lutz Schröder, Till Mossakowski |
| Editor: |
Rastislav Kralovic, Pawel Urzyczyn |
| Title: |
Completeness of Global Evaluation Logic |
| Book / Collection title: |
Mathematical Foundations of Computer Science |
| Volume: |
4162 |
| Page(s): |
447 – 458 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2006 |
| Publisher: |
Springer, Berlin |
| 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.
|
| Internet: |
http://dx.doi.org/10.1007/11821069_39 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/GELcompl.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/GELcompl.ps |
| Keywords: |
side effects monads evaluation logic completeness |
| Status: |
Reviewed |
| Last updated: |
18. 06. 2008 |
