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 show how to define the Dijkstra monad associated with , via the logic involved. Technically, we provide a morphism of monads from the state monad transformation applied to , to the Dijkstra monad associated with . This monad map is precisely the weakest precondition map in the triangle, given in categorical terms by substitution. © 2014 IFIP International Federation for Information Processing.
CITATION STYLE
Jacobs, B. (2014). Dijkstra monads in monadic computation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8446 LNCS, pp. 135–150). Springer Verlag. https://doi.org/10.1007/978-3-662-44124-4_8
Mendeley helps you to discover research relevant for your work.