{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:11Z","timestamp":1772164091036,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,7]],"date-time":"2017-09-07T00:00:00Z","timestamp":1504742400000},"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,9,7]]},"DOI":"10.1145\/3122955.3122962","type":"proceedings-article","created":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T08:27:52Z","timestamp":1504254472000},"page":"52-62","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Using Coq to write fast and correct Haskell"],"prefix":"10.1145","author":[{"given":"John","family":"Wiegley","sequence":"first","affiliation":[{"name":"BAE Systems, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,9,7]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088355"},{"key":"e_1_3_2_2_2_1","volume-title":"Category Theory","author":"Awodey S.","unstructured":"S. Awodey . 2006. Category Theory . Ebsco Publishing . https:\/\/books.google.com\/ books?id=IK_sIDI2TCwC S. Awodey. 2006. Category Theory. Ebsco Publishing. https:\/\/books.google.com\/ books?id=IK_sIDI2TCwC"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_3_2_2_5_1","volume-title":"Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant","author":"Delaware Benjamin","year":"2015","unstructured":"Benjamin Delaware , Cl\u00e9ment Pit-Claudel , Jason Gross , and Adam Chlipala . 2015 . Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant . Association for Computing Machinery . http:\/\/dspace.mit.edu\/handle\/1721.1\/91993 Benjamin Delaware, Cl\u00e9ment Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. Association for Computing Machinery. http:\/\/dspace.mit.edu\/handle\/1721.1\/91993"},{"key":"e_1_3_2_2_6_1","volume-title":"A constructive approach to the problem of program correctness. (Aug","author":"Dijkstra Edsger W.","year":"1967","unstructured":"Edsger W. Dijkstra . 1967. A constructive approach to the problem of program correctness. (Aug . 1967 ). http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd02xx\/EWD209. PDF Circulated privately. Edsger W. Dijkstra. 1967. A constructive approach to the problem of program correctness. (Aug. 1967). http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd02xx\/EWD209. PDF Circulated privately."},{"key":"e_1_3_2_2_7_1","volume-title":"Dependent Types in Haskell: Theory and Practice. CoRR abs\/1610.07978","author":"Eisenberg Richard A.","year":"2016","unstructured":"Richard A. Eisenberg . 2016. Dependent Types in Haskell: Theory and Practice. CoRR abs\/1610.07978 ( 2016 ). https:\/\/www.cis.upenn.edu\/~sweirich\/papers\/ eisenberg-thesis.pdf Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. CoRR abs\/1610.07978 (2016). https:\/\/www.cis.upenn.edu\/~sweirich\/papers\/ eisenberg-thesis.pdf"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993504"},{"key":"e_1_3_2_2_9_1","volume-title":"Lecture Notes in Computer Science","volume":"213","author":"He J.","unstructured":"J. He , C.A.R. Hoare , and J.W. Sanders . 1986. Data refinement refined. In ESOP 86, Bernard Robinet and Reinhard Wilhelm (Eds.) . Lecture Notes in Computer Science , Vol. 213 . Springer Berlin Heidelberg, 187\u2013196. J. He, C.A.R. Hoare, and J.W. Sanders. 1986. Data refinement refined. In ESOP 86, Bernard Robinet and Reinhard Wilhelm (Eds.). Lecture Notes in Computer Science, Vol. 213. Springer Berlin Heidelberg, 187\u2013196."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"e_1_3_2_2_12_1","series-title":"Lecture Notes in Computer Science","volume-title":"Refinement to Imperative\/HOL","author":"Lammich Peter","unstructured":"Peter Lammich . 2015. Refinement to Imperative\/HOL . In Interactive Theorem Proving, Christian Urban and Xingyuan Zhang (Eds.). Lecture Notes in Computer Science , Vol. 9236 . Springer International Publishing , 253\u2013269. DOI: Peter Lammich. 2015. Refinement to Imperative\/HOL. In Interactive Theorem Proving, Christian Urban and Xingyuan Zhang (Eds.). Lecture Notes in Computer Science, Vol. 9236. Springer International Publishing, 253\u2013269. DOI:"},{"key":"e_1_3_2_2_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Applying Data Refinement for Monadic Programs to Hopcroft\u00e2\u0102\u0179s Algorithm","author":"Lammich Peter","unstructured":"Peter Lammich and Thomas Tuerk . 2012. Applying Data Refinement for Monadic Programs to Hopcroft\u00e2\u0102\u0179s Algorithm . In Interactive Theorem Proving, Lennart Beringer and Amy Felty (Eds.). Lecture Notes in Computer Science , Vol. 7406 . Springer Berlin Heidelberg , 166\u2013182. Peter Lammich and Thomas Tuerk. 2012. Applying Data Refinement for Monadic Programs to Hopcroft\u00e2\u0102\u0179s Algorithm. In Interactive Theorem Proving, Lennart Beringer and Amy Felty (Eds.). Lecture Notes in Computer Science, Vol. 7406. Springer Berlin Heidelberg, 166\u2013182."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_15_1","volume-title":"Proc","author":"Letouzey Pierre","unstructured":"Pierre Letouzey . 2003. A New Extraction for Coq . In Proc . TYPES. Springer-Verlag . Pierre Letouzey. 2003. A New Extraction for Coq. In Proc. TYPES. Springer-Verlag."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908122"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357177"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542522"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775050.2633366"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110269"},{"key":"e_1_3_2_2_22_1","unstructured":"Edward Yang. 2010. How to pick your string library in Haskell. http:\/\/blog. ezyang.com\/2010\/08\/strings-in-haskell\/ . (2010).  Edward Yang. 2010. How to pick your string library in Haskell. http:\/\/blog. ezyang.com\/2010\/08\/strings-in-haskell\/ . (2010)."}],"event":{"name":"ICFP '17: ACM SIGPLAN International Conference on Functional Programming","location":"Oxford UK","acronym":"ICFP '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3122955.3122962","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3122955.3122962","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:11:04Z","timestamp":1750198264000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3122955.3122962"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,7]]},"references-count":22,"alternative-id":["10.1145\/3122955.3122962","10.1145\/3122955"],"URL":"https:\/\/doi.org\/10.1145\/3122955.3122962","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3156695.3122962","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,9,7]]},"assertion":[{"value":"2017-09-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}