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.
Type de document :
Communication dans un congrès
Marcello M. Bonsangue. 12th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2014, Grenoble, France. Lecture Notes in Computer Science, LNCS-8446, pp.135-150, 2014, Coalgebraic Methods in Computer Science. 〈10.1007/978-3-662-44124-4_8〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01408757
Contributeur : Hal Ifip <>
Soumis le : lundi 5 décembre 2016 - 13:24:57
Dernière modification le : lundi 5 décembre 2016 - 14:32:53
Document(s) archivé(s) le : mardi 21 mars 2017 - 10:42:43

Fichier

328263_1_En_8_Chapter.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Bart Jacobs. Dijkstra Monads in Monadic Computation. Marcello M. Bonsangue. 12th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2014, Grenoble, France. Lecture Notes in Computer Science, LNCS-8446, pp.135-150, 2014, Coalgebraic Methods in Computer Science. 〈10.1007/978-3-662-44124-4_8〉. 〈hal-01408757〉

Partager

Métriques

Consultations de la notice

24

Téléchargements de fichiers

85