{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:54Z","timestamp":1772164074497,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,8,30]],"date-time":"2015-08-30T00:00:00Z","timestamp":1440892800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1117569"],"award-info":[{"award-number":["1117569"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,8,30]]},"DOI":"10.1145\/2804302.2804303","type":"proceedings-article","created":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T10:09:20Z","timestamp":1440410960000},"page":"23-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs"],"prefix":"10.1145","author":[{"given":"Andrew","family":"Farmer","sequence":"first","affiliation":[{"name":"University of Kansas, USA"}]},{"given":"Neil","family":"Sculthorpe","sequence":"additional","affiliation":[{"name":"University of Kansas, USA \/ Swansea University, UK"}]},{"given":"Andy","family":"Gill","sequence":"additional","affiliation":[{"name":"University of Kansas, USA"}]}],"member":"320","published-online":{"date-parts":[[2015,8,30]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2543728.2543730"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1951654"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_14"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628141"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"e_1_3_2_1_8_1","first-page":"109","volume-title":"International Conference on Mathematics of Program Construction","volume":"3125","author":"Danielsson N. A.","unstructured":"N. A. Danielsson and P. Jansson . Chasing bottoms: A case study in program verification in the presence of partial and infinite values . In International Conference on Mathematics of Program Construction , volume 3125 of LNCS, pages 85\u2013 109 . Springer, 2004. N. A. Danielsson and P. Jansson. Chasing bottoms: A case study in program verification in the presence of partial and infinite values. In International Conference on Mathematics of Program Construction, volume 3125 of LNCS, pages 85\u2013109. Springer, 2004."},{"key":"e_1_3_2_1_10_1","first-page":"944","volume-title":"International Joint Conference on Artificial Intelligence","volume":"2","author":"Dershowitz N.","unstructured":"N. Dershowitz , J. Hsiang , N. A. Josephson , and D. A. Plaisted . Associative-commutative rewriting . In International Joint Conference on Artificial Intelligence , volume 2 , pages 940\u2013 944 . Morgan Kaufmann, 1983. N. Dershowitz, J. Hsiang, N. A. Josephson, and D. A. Plaisted. Associative-commutative rewriting. In International Joint Conference on Artificial Intelligence, volume 2, pages 940\u2013944. Morgan Kaufmann, 1983."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364508"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2543728.2543736"},{"key":"e_1_3_2_1_14_1","unstructured":"A. Farmer A. Gill E. Komp and N. Sculthorpe. http:\/\/hackage. haskell.org\/package\/hermit 2015.  A. Farmer A. Gill E. Komp and N. Sculthorpe. http:\/\/hackage. haskell.org\/package\/hermit 2015."},{"key":"e_1_3_2_1_15_1","volume-title":"Hermit case studies: Proving Type-Class Laws & Making a Century","author":"Farmer A.","year":"2015","unstructured":"A. Farmer , N. Sculthorpe , and A. Gill . Hermit case studies: Proving Type-Class Laws & Making a Century , 2015 . URL http:\/\/www. ittc.ku.edu\/csdl\/fpg\/HERMIT\/case-studies-2015\/. A. Farmer, N. Sculthorpe, and A. Gill. Hermit case studies: Proving Type-Class Laws & Making a Century, 2015. URL http:\/\/www. ittc.ku.edu\/csdl\/fpg\/HERMIT\/case-studies-2015\/."},{"key":"e_1_3_2_1_16_1","volume-title":"Version 7.8.4","author":"Team GHC","year":"2014","unstructured":"GHC Team . GHC User\u2019s Guide , Version 7.8.4 , 2014 . URL http: \/\/downloads.haskell.org\/~ghc\/7.8.4\/docs\/html. GHC Team. GHC User\u2019s Guide, Version 7.8.4, 2014. URL http: \/\/downloads.haskell.org\/~ghc\/7.8.4\/docs\/html."},{"issue":"4","key":"e_1_3_2_1_17_1","first-page":"353","article-title":"Proof methods for corecursive programs","volume":"66","author":"Gibbons J.","year":"2005","unstructured":"J. Gibbons and G. Hutton . Proof methods for corecursive programs . Fundamenta Informaticae , 66 ( 4 ): 353 \u2013 366 , 2005 . J. Gibbons and G. Hutton. Proof methods for corecursive programs. Fundamenta Informaticae, 66(4):353\u2013366, 2005.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159856"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007175"},{"issue":"2","key":"e_1_3_2_1_21_1","first-page":"173","article-title":"Tool support for the interactive derivation of formally correct functional programs","volume":"9","author":"Guttmann W.","year":"2003","unstructured":"W. Guttmann , H. Partsch , W. Schulte , and T. Vullinghs . Tool support for the interactive derivation of formally correct functional programs . Journal of Universal Computer Science , 9 ( 2 ): 173 \u2013 188 , 2003 . W. Guttmann, H. Partsch, W. Schulte, and T. Vullinghs. Tool support for the interactive derivation of formally correct functional programs. Journal of Universal Computer Science, 9(2):173\u2013188, 2003.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364514"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/968486.968488"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.02.053"},{"key":"e_1_3_2_1_25_1","first-page":"144","volume-title":"Conference on Functional Programming Languages and Computer Architecture","volume":"523","author":"Meijer E.","unstructured":"E. Meijer , M. M. Fokkinga , and R. Paterson . Functional programming with bananas, lenses, envelopes and barbed wire . In Conference on Functional Programming Languages and Computer Architecture , volume 523 of LNCS, pages 124\u2013 144 . Springer, 1991. E. Meijer, M. M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Conference on Functional Programming Languages and Computer Architecture, volume 523 of LNCS, pages 124\u2013144. Springer, 1991."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007345"},{"key":"e_1_3_2_1_27_1","first-page":"233","volume-title":"Haskell Workshop","author":"Peyton Jones S.","unstructured":"S. Peyton Jones , A. Tolmach , and T. Hoare . Playing by the rules: Rewriting as a practical optimisation technique in GHC . In Haskell Workshop , pages 203\u2013 233 . ACM, 2001. S. Peyton Jones, A. Tolmach, and T. Hoare. Playing by the rules: Rewriting as a practical optimisation technique in GHC. In Haskell Workshop, pages 203\u2013233. ACM, 2001."},{"key":"e_1_3_2_1_28_1","first-page":"70","volume-title":"International Symposium on Implementation and Application of Functional Languages","volume":"8241","author":"Reich J. S.","unstructured":"J. S. Reich , M. Naylor , and C. Runciman . Advances in lazy smallcheck . In International Symposium on Implementation and Application of Functional Languages , volume 8241 of LNCS, pages 53\u2013 70 . Springer, 2013. J. S. Reich, M. Naylor, and C. Runciman. Advances in lazy smallcheck. In International Symposium on Implementation and Application of Functional Languages, volume 8241 of LNCS, pages 53\u201370. Springer, 2013."},{"key":"e_1_3_2_1_29_1","series-title":"LNCS","first-page":"423","volume-title":"Colloque sur la Programmation","author":"Reynolds J. C.","unstructured":"J. C. Reynolds . Towards a theory of type structure . In Colloque sur la Programmation , volume 19 of LNCS , pages 408\u2013 423 . Springer, 1974. J. C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, volume 19 of LNCS, pages 408\u2013423. Springer, 1974."},{"key":"e_1_3_2_1_30_1","volume-title":"Proving equational Haskell properties using automated theorem provers. Master\u2019s thesis","author":"Ros\u00e9n D.","year":"2012","unstructured":"D. Ros\u00e9n . Proving equational Haskell properties using automated theorem provers. Master\u2019s thesis , University of Gothenburg , 2012 . D. Ros\u00e9n. Proving equational Haskell properties using automated theorem provers. Master\u2019s thesis, University of Gothenburg, 2012."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000045"},{"key":"e_1_3_2_1_33_1","first-page":"103","volume-title":"International Symposium on Implementation and Application of Functional Languages","volume":"8241","author":"Sculthorpe N.","unstructured":"N. Sculthorpe , A. Farmer , and A. Gill . The HERMIT in the tree: Mechanizing program transformations in the GHC core language . In International Symposium on Implementation and Application of Functional Languages , volume 8241 of LNCS, pages 86\u2013 103 . Springer, 2013. N. Sculthorpe, A. Farmer, and A. Gill. The HERMIT in the tree: Mechanizing program transformations in the GHC core language. In International Symposium on Implementation and Application of Functional Languages, volume 8241 of LNCS, pages 86\u2013103. Springer, 2013."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000185"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_2_1_38_1","series-title":"LNCS","first-page":"179","volume-title":"Algebraic Methodology and Software Technology","author":"Tesson J.","unstructured":"J. Tesson , H. Hashimoto , Z. Hu , F. Loulergue , and M. Takeichi . Program calculation in Coq . In Algebraic Methodology and Software Technology , volume 6486 of LNCS , pages 163\u2013 179 . Springer, 2011. J. Tesson, H. Hashimoto, Z. Hu, F. Loulergue, and M. Takeichi. Program calculation in Coq. In Algebraic Methodology and Software Technology, volume 6486 of LNCS, pages 163\u2013179. Springer, 2011."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000117"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_43_1","first-page":"38","volume-title":"International Conference on Rewriting Techniques and Applications","author":"Vytiniotis D.","unstructured":"D. Vytiniotis and S. Peyton Jones . Evidence normalization in System FC . In International Conference on Rewriting Techniques and Applications , pages 20\u2013 38 . Schloss Dagstuhl, 2013. D. Vytiniotis and S. Peyton Jones. Evidence normalization in System FC. In International Conference on Rewriting Techniques and Applications, pages 20\u201338. Schloss Dagstuhl, 2013."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"}],"event":{"name":"ICFP'15: 20th ACM SIGPLAN International Conference on Functional Programming","location":"Vancouver BC Canada","acronym":"ICFP'15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2804302.2804303","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2804302.2804303","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:07:09Z","timestamp":1750208829000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2804302.2804303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,30]]},"references-count":41,"alternative-id":["10.1145\/2804302.2804303","10.1145\/2804302"],"URL":"https:\/\/doi.org\/10.1145\/2804302.2804303","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2887747.2804303","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,8,30]]},"assertion":[{"value":"2015-08-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}