{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:15:51Z","timestamp":1787066151268,"version":"build-2736575974"},"reference-count":51,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2022,10,28]],"date-time":"2022-10-28T00:00:00Z","timestamp":1666915200000},"content-version":"unspecified","delay-in-days":210,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Weakest precondition transformers are useful tools in program verification. One of their key properties is composability, that is, the weakest precondition predicate transformer (wppt for short) associated to program\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000330_inline1.png\"\/>\n                        <jats:tex-math>$f;\\;g$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    should be equal to the composition of the wppts associated to\n                    <jats:italic>f<\/jats:italic>\n                    and\n                    <jats:italic>g<\/jats:italic>\n                    . In this paper, we study the categorical structure behind wppts from a fibrational point of view. We characterize the wppts that satisfy composability as the ones constructed from the Cartesian lifting of a monad. We moreover show that Cartesian liftings of monads along lax slice categories bijectively correspond to Eilenberg\u2013Moore monotone algebras. We then instantiate our techniques by deriving wppts for commonplace effects such as the maybe monad, the nonempty powerset monad, the counter monad, or the distribution monad. We also show how to combine them to derive the wppts appearing in the literature of verification of probabilistic programs.\n                  <\/jats:p>","DOI":"10.1017\/s0960129522000330","type":"journal-article","created":{"date-parts":[[2022,10,28]],"date-time":"2022-10-28T07:17:08Z","timestamp":1666941428000},"page":"472-510","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":8,"title":["Weakest preconditions in fibrations"],"prefix":"10.1017","volume":"32","author":[{"given":"Alejandro","family":"Aguirre","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7529-5489","authenticated-orcid":false,"given":"Shin-ya","family":"Katsumata","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Satoshi","family":"Kura","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,10,28]]},"reference":[{"key":"S0960129522000330_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_33"},{"key":"S0960129522000330_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.047"},{"key":"S0960129522000330_ref15","doi-asserted-by":"crossref","unstructured":"Hermida, C. (1993). Fibrations, Logical Predicates and Indeterminants. Phd thesis, University of Edinburgh.","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"S0960129522000330_ref21","doi-asserted-by":"crossref","unstructured":"Katsumata, S. (2005). A semantic formulation of $\\top\\top$ -lifting and logical predicates for computational metalanguage. In: Proceedings of CSL\u201905, LNCS, vol. 3634, Springer, 87\u2013102.","DOI":"10.1007\/11538363_8"},{"key":"#cr-split#-S0960129522000330_ref40.1","doi-asserted-by":"crossref","unstructured":"Pitts, A. M. (1999). Tripos theory in retrospect. Electronic Notes in Theoretical Computer Science 23","DOI":"10.1016\/S1571-0661(04)00107-0"},{"key":"#cr-split#-S0960129522000330_ref40.2","unstructured":"(1) 111-127. Tutorial Workshop on Realizability Semantics and Applications (associated to FLoC'99, the 1999 Federated Logic Conference)."},{"key":"S0960129522000330_ref30","doi-asserted-by":"crossref","unstructured":"Maillard, K. , Ahman, D. , Atkey, R. , Martnez, G. , Hritcu, C. , Rivas, E. and Tanter, \u00c9. (2019). Dijkstra monads for all. Proceedings of the ACM on Programming Languages 3 (ICFP) 104:1\u2013104:29.","DOI":"10.1145\/3341708"},{"key":"S0960129522000330_ref49","unstructured":"whiskering Whiskering. https:\/\/ncatlab.org\/nlab\/show\/whiskering."},{"key":"S0960129522000330_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.09.002"},{"key":"S0960129522000330_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3527310"},{"key":"S0960129522000330_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"S0960129522000330_ref47","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"},{"key":"S0960129522000330_ref9","unstructured":"Filinski, A. (1996). Controlling Effects. Phd thesis, Carnegie Mellon University."},{"key":"S0960129522000330_ref22","article-title":"Codensity lifting of monads and its dual","volume":"14","author":"Katsumata","year":"2018","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129522000330_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129522000330_ref25","first-page":"135","author":"Kura","year":"2019"},{"key":"S0960129522000330_ref27","unstructured":"Leino, K. R. M. and van de Snepscheut, J. L. A. (1994). Semantics of exceptions. In: Olderog, E.-R. (ed.) Programming Concepts, Methods and Calculi, Proceedings of the IFIP TC2\/WG2.1\/WG2.2\/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET\u201994) San Miniato, Italy, 6\u201310 June, 1994, IFIP Transactions, vol. A-56, North-Holland, 447\u2013466."},{"key":"S0960129522000330_ref38","doi-asserted-by":"publisher","DOI":"10.14232\/actacyb.24.3.2020.2"},{"key":"S0960129522000330_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304852"},{"key":"S0960129522000330_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007172"},{"key":"S0960129522000330_ref43","unstructured":"Sato, T. (2011). A probabilistic monad with nondeterminism for coalgebraic trace semantics. tetsuya sato. In: CALCO Young Researchers Workshop CALCO-jnr 2011 Selected Papers, University of Southampton."},{"key":"S0960129522000330_ref44","doi-asserted-by":"publisher","DOI":"10.4018\/978-1-60960-747-0.ch002"},{"key":"S0960129522000330_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90020-5"},{"key":"S0960129522000330_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"S0960129522000330_ref24","unstructured":"Kura, S. (2022). Semantic Refinements for Program Verification. Phd thesis, The Graduate University for Advanced Studies, SOKENDAI."},{"key":"S0960129522000330_ref50","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.02.008"},{"key":"S0960129522000330_ref7","unstructured":"Bonchi, F. , K\u00f6nig, B. and Petrisan, D. (2018). Up-to techniques for behavioural metrics via fibrations. In: Schewe, S. and Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4\u20137, 2018, Beijing, China, LIPIcs, vol. 118, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 17:1\u201317:17."},{"key":"S0960129522000330_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60915-6_2"},{"key":"S0960129522000330_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"S0960129522000330_ref18","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"141","author":"Jacobs","year":"1999"},{"key":"S0960129522000330_ref28","volume-title":"London Mathematical Society Lecture Note Series","author":"Leinster","year":"2004"},{"key":"S0960129522000330_ref29","volume-title":"Categories for the Working Mathematician","volume":"5","author":"MacLane","year":"1998"},{"key":"S0960129522000330_ref31","doi-asserted-by":"crossref","unstructured":"Maillard, K. , Hritcu, C. , Rivas, E. and Van Muylder, A. (2020). The next 700 relational program logics. Proceedings of the ACM on Programming Languages 4 (POPL) 4:1\u20134:33.","DOI":"10.1145\/3371072"},{"key":"S0960129522000330_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935319"},{"key":"S0960129522000330_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80970-8"},{"key":"S0960129522000330_ref42","doi-asserted-by":"crossref","unstructured":"Rauch, C. , Goncharov, S. and Schr\u00f6der, L. (2016). Generic hoare logic for order-enriched effects with exceptions. In: James, P. and Roggenbach, M. (eds.) Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21\u201324, 2016, Revised Selected Papers, Lecture Notes in Computer Science, vol. 10644, Springer, 208\u2013222.","DOI":"10.1007\/978-3-319-72044-9_14"},{"key":"S0960129522000330_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90019-9"},{"key":"S0960129522000330_ref26","volume-title":"Universitext","author":"Lane","year":"1994"},{"key":"S0960129522000330_ref46","first-page":"1","article-title":"Relatively complete refinement type system for verification of higher-order non-deterministic programs","volume":"2","author":"Unno","year":"2018","journal-title":"PACMPL"},{"key":"S0960129522000330_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.015"},{"key":"S0960129522000330_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.027"},{"key":"S0960129522000330_ref32","first-page":"172","article-title":"Monad compositions I: general constructions and recursive distributive laws","volume":"18","author":"Manes","year":"2007","journal-title":"Theory and Applications of Categories"},{"key":"S0960129522000330_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676970"},{"key":"S0960129522000330_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3434333"},{"key":"S0960129522000330_ref11","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.33"},{"key":"S0960129522000330_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100074338"},{"key":"S0960129522000330_ref34","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"McIver","year":"2005"},{"key":"S0960129522000330_ref37","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1995-22126"},{"key":"S0960129522000330_ref39","author":"Pitts","year":"1991"},{"key":"S0960129522000330_ref13","doi-asserted-by":"crossref","unstructured":"Goy, A. and Petrisan, D. (2020). Combining probabilistic and non-deterministic choice via weak distributive laws. In: Hermanns, H., Zhang, L., Kobayashi, N. and Miller, D. (eds.) LICS\u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, July 8\u201311, 2020, ACM, 454\u2013464.","DOI":"10.1145\/3373718.3394795"},{"key":"S0960129522000330_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0083084"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000330","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,16]],"date-time":"2022-12-16T07:26:53Z","timestamp":1671175613000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000330\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4]]},"references-count":51,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["S0960129522000330"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000330","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}