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

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

https://hal.inria.fr/hal-01408750
Contributeur : Hal Ifip <>
Soumis le : lundi 5 décembre 2016 - 13:21:15
Dernière modification le : lundi 5 décembre 2016 - 13:23:33
Document(s) archivé(s) le : lundi 20 mars 2017 - 21:25:00

Fichier

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

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

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

Partager

Métriques

Consultations de la notice

57

Téléchargements de fichiers

4