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.
Users
Please
log in to take part in the discussion (add own reviews or comments).