Publikation
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, Pages 447-458, Lecture Notes in Computer Science (LNCS), Vol. 4162, Springer; http://www.springer.de, Berlin, 2006.
Zusammenfassung
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.