Dijkstra Monads in Monadic Computation

Abstract : The Dijkstra monad has been introduced recently for capturing weakest precondition computations within the context of program verification, supported by a theorem prover. Here we give a more general description of such Dijkstra monads in a categorical setting. We first elaborate the recently developed view on program semantics in terms of a triangle of computations, state transformers, and predicate transformers. Instantiations of this triangle for different monads T show how to define the Dijkstra monad associated with T , via the logic involved. Technically, we provide a morphism of monads from the state monad transformation applied to T , to the Dijkstra monad associated with T . This monad map is precisely the weakest precondition map in the triangle, given in categorical terms by substitution.
Document type :
Conference papers
Complete list of metadatas

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01408757
Contributor : Hal Ifip <>
Submitted on : Monday, December 5, 2016 - 1:24:57 PM
Last modification on : Monday, December 5, 2016 - 2:32:53 PM
Long-term archiving on : Tuesday, March 21, 2017 - 10:42:43 AM

File

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

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Bart Jacobs. Dijkstra Monads in Monadic Computation. 12th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2014, Grenoble, France. pp.135-150, ⟨10.1007/978-3-662-44124-4_8⟩. ⟨hal-01408757⟩

Share

Metrics

Record views

57

Files downloads

223