We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs' recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: (1) different notions of modality (such as "may" vs. "must") are captured by Eilenberg-Moore algebras; (2) nested branching-like in games and in probabilistic systems with nondeterministic environments-is modularly modeled by a monad on the Eilenberg-Moore category of another. © 2014 IFIP International Federation for Information Processing.
CITATION STYLE
Hasuo, I. (2014). Generic weakest precondition semantics from monads enriched with order. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8446 LNCS, pp. 10–32). Springer Verlag. https://doi.org/10.1007/978-3-662-44124-4_2
Mendeley helps you to discover research relevant for your work.