Completeness of Global Evaluation Logic (bibtex)
by Sergey Goncharov, Lutz Schröder, 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:
Completeness of Global Evaluation Logic (Sergey Goncharov, Lutz Schröder, Till Mossakowski), In Mathematical Foundations of Computer Science (Rastislav Královič, Paweł Urzyczyn, eds.), Lecture Notes in Computer Science, vol. 4162, pp. 447–458, Springer, 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 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},
  comment={<a href="http://www.informatik.uni-bremen.de/~lschrode/papers/GELcompl.pdf">[preprint]</a>}, 
  psurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/GELcompl.ps},
  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.
},
}
Powered by bibtexbrowser