{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:55Z","timestamp":1775790715176,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009878","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"515-529","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Dijkstra monads for free"],"prefix":"10.1145","author":[{"given":"Danel","family":"Ahman","sequence":"first","affiliation":[{"name":"University of Edinburgh, UK \/ Microsoft Research, USA"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"Inria, France \/ Microsoft Research, USA"}]},{"given":"Kenji","family":"Maillard","sequence":"additional","affiliation":[{"name":"Inria, France \/ ENS, France \/ Microsoft Research, USA"}]},{"given":"Guido","family":"Mart\u00ednez","sequence":"additional","affiliation":[{"name":"Inria, France \/ Rosario National University, Argentina"}]},{"given":"Gordon","family":"Plotkin","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK \/ Microsoft Research, USA"}]},{"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"TYPES","author":"Ahman D.","year":"2013","unstructured":"D. Ahman and T. Uustalu . Update monads: Cointerpreting directed containers . TYPES , 2013 . D. Ahman and T. Uustalu. Update monads: Cointerpreting directed containers. TYPES, 2013."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_3"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050041"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/503032.503043"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004099"},{"key":"e_1_3_2_1_9_1","volume-title":"Monads and effects. APPSEM","author":"Benton N.","year":"2000","unstructured":"N. Benton , J. Hughes , and E. Moggi . Monads and effects. APPSEM . 2000 . N. Benton, J. Hughes, and E. Moggi. Monads and effects. APPSEM. 2000."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_3_2_1_11_1","volume-title":"TFP","author":"Brady E.","year":"2014","unstructured":"E. Brady . Resource-dependent algebraic effects . TFP , 2014 . E. Brady. Resource-dependent algebraic effects. TFP, 2014."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_3_2_1_13_1","volume-title":"Characteristic formulae for the verification of imperative programs. ICFP","author":"Chargu\u00e9raud A.","year":"2011","unstructured":"A. Chargu\u00e9raud . Characteristic formulae for the verification of imperative programs. ICFP . 2011 . A. Chargu\u00e9raud. Characteristic formulae for the verification of imperative programs. ICFP. 2011."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_16_1","volume-title":"Z3: an efficient SMT solver. TACAS","author":"de Moura L. M.","year":"2008","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Z3: an efficient SMT solver. TACAS . 2008 . L. M. de Moura and N. Bj\u00f8rner. Z3: an efficient SMT solver. TACAS. 2008."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/550359"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292557"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706354"},{"key":"e_1_3_2_1_22_1","volume-title":"Why3 \u2014 where programs meet provers. ESOP","author":"Filli\u02c6atre J.-C.","year":"2013","unstructured":"J.-C. Filli\u02c6atre and A. Paskevich . Why3 \u2014 where programs meet provers. ESOP . 2013 . J.-C. Filli\u02c6atre and A. Paskevich. Why3 \u2014 where programs meet provers. ESOP. 2013."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.020"},{"key":"e_1_3_2_1_25_1","volume-title":"Connection between Dijkstra\u2019s predicate-transformers and denotational continuation-semantics. DAIMI Report Series 7.86","author":"Jensen K.","year":"1978","unstructured":"K. Jensen . Connection between Dijkstra\u2019s predicate-transformers and denotational continuation-semantics. DAIMI Report Series 7.86 , 1978 . K. Jensen. Connection between Dijkstra\u2019s predicate-transformers and denotational continuation-semantics. DAIMI Report Series 7.86, 1978."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.016"},{"key":"e_1_3_2_1_27_1","volume-title":"Mixed powerdomains for probability and nondeterminism. submitted to LMCS","author":"Keimel K.","year":"2016","unstructured":"K. Keimel and G. Plotkin . Mixed powerdomains for probability and nondeterminism. submitted to LMCS , 2016 . K. Keimel and G. Plotkin. Mixed powerdomains for probability and nondeterminism. submitted to LMCS, 2016."},{"key":"e_1_3_2_1_28_1","volume-title":"Dafny: An automatic program verifier for functional correctness. LPAR","author":"Leino K. R. M.","year":"2010","unstructured":"K. R. M. Leino . Dafny: An automatic program verifier for functional correctness. LPAR . 2010 . K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. LPAR. 2010."},{"key":"e_1_3_2_1_29_1","volume-title":"Computational lambda-calculus and monads. LICS","author":"Moggi E.","year":"1989","unstructured":"E. Moggi . Computational lambda-calculus and monads. LICS . 1989 . E. Moggi. Computational lambda-calculus and monads. LICS. 1989."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_2_1_31_1","volume-title":"Quotient types: A modular approach. TPHOLs","author":"Nogin A.","year":"2002","unstructured":"A. Nogin . Quotient types: A modular approach. TPHOLs . 2002 . A. Nogin. Quotient types: A modular approach. TPHOLs. 2002."},{"key":"e_1_3_2_1_32_1","series-title":"Studies in Logic (Mathematical logic and foundations)","volume-title":"All about Proofs, Proofs for All","author":"Paulin-Mohring C.","year":"2015","unstructured":"C. Paulin-Mohring . Introduction to the Calculus of Inductive Constructions . In B. W. Paleo and D. Delahaye, editors, All about Proofs, Proofs for All , volume 55 of Studies in Logic (Mathematical logic and foundations) . College Publications , 2015 . C. Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. In B. W. Paleo and D. Delahaye, editors, All about Proofs, Proofs for All, volume 55 of Studies in Logic (Mathematical logic and foundations). College Publications, 2015."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2096148.2034688"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034778"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019944"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009878","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009878","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:34Z","timestamp":1750259134000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009878"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":41,"alternative-id":["10.1145\/3009837.3009878","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009878","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009878","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}