{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:58:40Z","timestamp":1770289120444,"version":"3.49.0"},"reference-count":44,"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>Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.<\/jats:p>","DOI":"10.1145\/3341707","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["A predicate transformer semantics for effects (functional pearl)"],"prefix":"10.1145","volume":"3","author":[{"given":"Wouter","family":"Swierstra","sequence":"first","affiliation":[{"name":"Utrecht University, Netherlands"}]},{"given":"Tim","family":"Baanen","sequence":"additional","affiliation":[{"name":"Utrecht University, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.04.003"},{"key":"e_1_2_2_3_1","volume-title":"Indexed containers. Journal of Functional Programming 25","author":"Altenkirch Thorsten","year":"2015"},{"key":"e_1_2_2_4_1","volume-title":"Refinement calculus: a systematic introduction","author":"Back Ralph-Johan"},{"key":"e_1_2_2_5_1","volume-title":"Refinement Concepts Formalized in Higher Order Logic. Formal Aspects of Computing 2","author":"Back R. J. R.","year":"1989"},{"key":"e_1_2_2_6_1","volume-title":"Pearls of Functional Algorithm Design","author":"Bird Richard"},{"key":"e_1_2_2_7_1","volume-title":"The algebra of programming","author":"Bird Richard"},{"key":"e_1_2_2_8_1","volume-title":"Typed Lambda Calculi and Applications","author":"Boulm\u00e9 Sylvain"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000115"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_2_2_13_1","volume-title":"Proc. Conf. Formal Methods Pacific\u201997","author":"Butler M. J.","year":"1997"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_2_2_15_1","volume-title":"2nd Summit on Advances in Programming Languages (SNAPL","author":"Chlipala Adam","year":"2017"},{"key":"e_1_2_2_16_1","unstructured":"The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual version 8.7. ADT Coq (Action for Technological Development). http:\/\/coq.inria.fr  The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual version 8.7. ADT Coq (Action for Technological Development). http:\/\/coq.inria.fr"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_18_1","volume-title":"Mathematics of Program Construction (LNCS)","author":"Dongol Brijesh"},{"key":"e_1_2_2_19_1","volume-title":"Unifying Theories of Programming, Burkhart Wolff, Marie-Claude Gaudel","author":"Gibbons Jeremy"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"e_1_2_2_21_1","volume-title":"14th InternationalWorkshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21 \u2013 26, 2000 Proceedings, Peter G. Clote and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg","author":"Hancock Peter","year":"2000"},{"key":"e_1_2_2_22_1","volume-title":"Workshop on Subtyping and Dependent Types in Programming. INRIA, Ponte de Lima, Portugal, Article 5, 13 pages.","author":"Hancock Peter","year":"2000"},{"key":"e_1_2_2_23_1","unstructured":"Graham Hutton and Diana Fulger. 2008. Reasoning about effects: Seeing the wood through the trees. (2008).  Graham Hutton and Diana Fulger. 2008. Reasoning about effects: Seeing the wood through the trees. (2008)."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_10"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_2_28_1","unstructured":"Kenji Maillard Danel Ahman Robert Atkey Guido Martinez Catalin Hritcu Exequiel Rivas and \u00c9ric Tanter. 2019. Dijkstra Monads for All. (2019). arXiv: cs.PL\/1903.01237  Kenji Maillard Danel Ahman Robert Atkey Guido Martinez Catalin Hritcu Exequiel Rivas and \u00c9ric Tanter. 2019. Dijkstra Monads for All. (2019). arXiv: cs.PL\/1903.01237"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19797-5_13"},{"key":"e_1_2_2_30_1","volume-title":"Programming from specifications","author":"Morgan Carroll"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704856"},{"key":"e_1_2_2_36_1","volume-title":"Algebraic operations and generic effects. Applied categorical structures 11, 1","author":"Plotkin Gordon","year":"2003"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_30"},{"key":"e_1_2_2_44_1","volume-title":"FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings (LNCS)","volume":"9613","author":"Swierstra Wouter","year":"2016"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291201.1291206"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_20"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/24697.24706"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341707","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341707","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\/3341707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":44,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341707"],"URL":"https:\/\/doi.org\/10.1145\/3341707","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"}}]}}