| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Sergey Goncharov, Lutz Schröder, Till Mossakowski |
| Herausgeber: |
Rastislav Kralovic, Pawel Urzyczyn |
| Titel: |
Completeness of Global Evaluation Logic |
| Buch / Sammlungs-Titel: |
Mathematical Foundations of Computer Science |
| Band: |
4162 |
| Seite(n): |
447 – 458 |
| Serie / Reihe: |
Lecture Notes in Computer Science |
| Erscheinungsjahr: |
2006 |
| Verleger: |
Springer, Berlin |
| Abstract / Kurzbeschreibung: |
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 |
| Schlagworte: |
side effects monads evaluation logic completeness |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
18. 06. 2008 |
