Completeness of Global Evaluation Logic

Sergey Goncharov, Lutz Schröder, Till Mossakowski

In: Rastislav Kralovic , Pawel Urzyczyn (Hrsg.). Mathematical Foundations of Computer Science. International Symposium on Mathematical Foundations of Computer Science (MFCS-2006) August 28-September 1 Stará Lesná Slovakia Seiten 447-458 Lecture Notes in Computer Science (LNCS) 4162 Springer; Berlin 2006.


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.

Weitere Links

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence