Generic Weakest Precondition Semantics from Monads Enriched with Order

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-01408750
Contributor : Hal Ifip <>
Submitted on : Monday, December 5, 2016 - 1:21:15 PM
Last modification on : Monday, December 5, 2016 - 1:23:33 PM
Long-term archiving on : Monday, March 20, 2017 - 9:25:00 PM

File

328263_1_En_2_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Ichiro Hasuo. Generic Weakest Precondition Semantics from Monads Enriched with Order. 12th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2014), Apr 2014, Grenoble, France. pp.10-32, ⟨10.1007/978-3-662-44124-4_2⟩. ⟨hal-01408750⟩

Share

Metrics

Record views

103

Files downloads

77