{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:02:49Z","timestamp":1760043769534,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T00:00:00Z","timestamp":1565222400000},"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":[[2019,8,8]]},"DOI":"10.1145\/3331545.3342592","type":"proceedings-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:51:45Z","timestamp":1564433505000},"page":"125-138","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Verifying effectful Haskell programs in Coq"],"prefix":"10.1145","author":[{"given":"Jan","family":"Christiansen","sequence":"first","affiliation":[{"name":"Flensburg University of Applied Sciences, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandra","family":"Dylus","sequence":"additional","affiliation":[{"name":"University of Kiel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niels","family":"Bunkenburg","sequence":"additional","affiliation":[{"name":"University of Kiel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,8,8]]},"reference":[{"volume-title":"Foundations of Software Science and Computation Structures.","author":"Abbott Michael","key":"e_1_3_2_1_1_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088355"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1721654.1721675"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Robert Atkey and Patricia Johann. 2015. Interleaving Data and Effects. Journal of Functional Programming 25 (2015).  Robert Atkey and Patricia Johann. 2015. Interleaving Data and Effects. Journal of Functional Programming 25 (2015).","DOI":"10.1017\/S0956796815000209"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Richard Bird. 2010. Pearls of Functional Algorithm Design. Cambridge University Press.   Richard Bird. 2010. Pearls of Functional Algorithm Design. Cambridge University Press.","DOI":"10.1017\/CBO9780511763199"},{"volume-title":"Typed Lambda Calculi and Applications.","author":"Bove Ana","key":"e_1_3_2_1_6_1"},{"key":"e_1_3_2_1_7_1","unstructured":"Joachim Breitner Antal Spector-Zabusky Yao Li Christine Rizkallah John Wiegley and Stephanie Weirich. 2018. Ready Set Verify! Applying Hs-to-Coq to Real-World Haskell Code. arXiv:1803.06960 {cs} (2018). arXiv: cs\/1803.06960  Joachim Breitner Antal Spector-Zabusky Yao Li Christine Rizkallah John Wiegley and Stephanie Weirich. 2018. Ready Set Verify! Applying Hs-to-Coq to Real-World Haskell Code. arXiv:1803.06960 {cs} (2018). arXiv: cs\/1803.06960"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Adam Chlipala. 2013. Certified Programming with Dependent Types. MIT Press New York.   Adam Chlipala. 2013. Certified Programming with Dependent Types. MIT Press New York.","DOI":"10.7551\/mitpress\/9153.001.0001"},{"volume-title":"Practical Aspects of Declarative Languages.","author":"Christiansen Jan","key":"e_1_3_2_1_9_1"},{"volume-title":"Implementation of Functional Languages.","author":"de Mol Maarten","key":"e_1_3_2_1_10_1"},{"key":"e_1_3_2_1_11_1","unstructured":"Gabe Dijkstra. 2012. Experimentation Project Report: Translating Haskell Programs to Coq Programs. (2012) 17.  Gabe Dijkstra. 2012. Experimentation Project Report: Translating Haskell Programs to Coq Programs. (2012) 17."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Sandra Dylus Jan Christiansen and Finn Teegen. 2019. One Monad to Prove Them All. The Art Science and Engineering of Programming 3 3 (2019).  Sandra Dylus Jan Christiansen and Finn Teegen. 2019. One Monad to Prove Them All. The Art Science and Engineering of Programming 3 3 (2019).","DOI":"10.22152\/programming-journal.org\/2019\/3\/8"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804303"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596556"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430532.2364514"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964010"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"volume-title":"Mathematics of Program Construction.","author":"McBride Conor","key":"e_1_3_2_1_20_1"},{"volume-title":"Tracing Monadic Computations and Representing Effects. Electronic Proceedings in Theoretical Computer Science 76 (Feb.","year":"2012","author":"Pir\u00f3g Maciej","key":"e_1_3_2_1_21_1"},{"key":"e_1_3_2_1_22_1","unstructured":"Andr\u00e9 L de M Santos. 1995. Compilation by Transformation in Non-Strict Functional Languages. (1995).  Andr\u00e9 L de M Santos. 1995. Compilation by Transformation in Non-Strict Functional Languages. (1995)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11964681_3"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"event":{"name":"ICFP '19: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Berlin Germany","acronym":"ICFP '19"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331545.3342592","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331545.3342592","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:39Z","timestamp":1750202019000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331545.3342592"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,8]]},"references-count":26,"alternative-id":["10.1145\/3331545.3342592","10.1145\/3331545"],"URL":"https:\/\/doi.org\/10.1145\/3331545.3342592","relation":{},"subject":[],"published":{"date-parts":[[2019,8,8]]},"assertion":[{"value":"2019-08-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}