{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:39Z","timestamp":1775790759501,"version":"3.50.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism between a computational monad and a specification monad gives rise to a Dijkstra monad, which provides great flexibility for obtaining Dijkstra monads tailored to the verification task at hand. We moreover show that a large variety of specification monads can be obtained by applying monad transformers to various base specification monads, including predicate transformers and Hoare-style pre- and postconditions. For defining correct monad transformers, we propose a language inspired by Moggi's monadic metalanguage that is parameterized by a dependent type theory. We also develop a notion of algebraic operations for Dijkstra monads, and start to investigate two ways of also accommodating effect handlers. We implement our framework in both Coq and F*, and illustrate that it supports a wide variety of verification styles for effects such as exceptions, nondeterminism, state, input-output, and general recursion.<\/jats:p>","DOI":"10.1145\/3341708","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Dijkstra monads for all"],"prefix":"10.1145","volume":"3","author":[{"given":"Kenji","family":"Maillard","sequence":"first","affiliation":[{"name":"Inria, France \/ ENS, France"}]},{"given":"Danel","family":"Ahman","sequence":"additional","affiliation":[{"name":"University of Ljubljana, Slovenia"}]},{"given":"Robert","family":"Atkey","sequence":"additional","affiliation":[{"name":"University of Strathclyde, UK"}]},{"given":"Guido","family":"Mart\u00ednez","sequence":"additional","affiliation":[{"name":"CIFASIS-CONICET, Argentina"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Exequiel","family":"Rivas","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile \/ Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Coproducts of monads on set . LICS","author":"Ad\u00e1mek J.","year":"2012"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158095"},{"key":"e_1_2_2_3_1","volume-title":"TYPES","author":"Ahman D.","year":"2013"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_2_5_1","volume-title":"Monads and effects . APPSEM","author":"Benton N.","year":"2000"},{"key":"e_1_2_2_6_1","volume-title":"Exploring the boundaries of monad tensorability on set . Logical Methods in Computer Science, 9(3)","author":"Bowler N.","year":"2013"},{"key":"e_1_2_2_7_1","volume-title":"The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories . Mathematical Structures in Computer Science, 24(6)","author":"Clairambault P.","year":"2014"},{"key":"e_1_2_2_8_1","volume-title":"COLOG","author":"Coquand T.","year":"1988"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500593"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"issue":"3","key":"e_1_2_2_11_1","first-page":"615","article-title":"The enriched effect calculus: syntax and semantics","volume":"24","author":"Egger J.","year":"2014","journal-title":"LogCom"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321422"},{"key":"e_1_2_2_13_1","volume-title":"A categorical approach to probability theory . Categorical Aspects of Topology and Analysis","author":"Giry M.","year":"1982"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.047"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.026"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.020"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.020"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.011"},{"key":"e_1_2_2_21_1","volume-title":"Signatures and induction principles for higher inductive-inductive types . arXiv:1902.00297","author":"Kaposi A.","year":"2019"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.014"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.10.015"},{"key":"e_1_2_2_25_1","volume-title":"Semantics of exceptions . PROCOMET","author":"Leino K. R. M.","year":"1994"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_20"},{"key":"e_1_2_2_28_1","volume-title":"Composing monads using coproducts . ICFP","author":"L\u00fcth C.","year":"2002"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.08.004"},{"key":"e_1_2_2_30_1","volume-title":"A sound and complete logic for algebraic effects . FoSSaCS","author":"Matache C.","year":"2019"},{"key":"e_1_2_2_31_1","volume-title":"Turing-completeness totally free . MPC","author":"McBride C.","year":"2015"},{"key":"e_1_2_2_32_1","volume-title":"Computational lambda-calculus and monads . LICS","author":"Moggi E.","year":"1989"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2383063.2383070"},{"key":"e_1_2_2_34_1","volume-title":"Programming from Specifications","author":"Morgan C.","year":"1994","edition":"2"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_2_40_1","volume-title":"IV Higher Order Workshop, Banff 1990","author":"Pitts A. M.","year":"1991"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704856"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_2_2_44_1","volume-title":"Handling algebraic effects . Logical Methods in Computer Science, 9(4)","author":"Plotkin G. D.","year":"2013"},{"key":"e_1_2_2_45_1","volume-title":"Microsoft Research Blog","author":"Protzenko J.","year":"2019"},{"key":"e_1_2_2_46_1","volume-title":"WADT","author":"Rauch C.","year":"2016"},{"key":"e_1_2_2_47_1","first-page":"35","volume-title":"Dependability and Computer Engineering: Concepts for Software-Intensive Systems","author":"Sekerinski E."},{"key":"e_1_2_2_48_1","volume-title":"Behavioural equivalence via modalities for algebraic effects . ESOP","author":"Simpson A.","year":"2018"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341707"},{"key":"e_1_2_2_52_1","volume-title":"Quantitative logics for equivalence of effectful programs . MFPS","author":"Voorneveld N.","year":"2019"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341708","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341708","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:23Z","timestamp":1750207403000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341708"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":51,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341708"],"URL":"https:\/\/doi.org\/10.1145\/3341708","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}