{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:56Z","timestamp":1779836756223,"version":"3.53.1"},"reference-count":55,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2021,2,26]],"date-time":"2021-02-26T00:00:00Z","timestamp":1614297600000},"content-version":"unspecified","delay-in-days":56,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Good tools can bring mechanical verification to programs written in mainstream functional languages. We use\n                    <jats:monospace>hs-to-coq<\/jats:monospace>\n                    to translate significant portions of Haskell\u2019s\n                    <jats:monospace>containers<\/jats:monospace>\n                    library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library\u2019s test suite, and interfaces from Coq\u2019s standard library. Our work shows that it is feasible to verify mature, widely used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend\n                    <jats:monospace>hs-to-coq<\/jats:monospace>\n                    to handle partiality, and \u2013 since we found no bugs \u2013 attest to the superb quality of well-tested functional code.\n                  <\/jats:p>","DOI":"10.1017\/s0956796820000283","type":"journal-article","created":{"date-parts":[[2021,2,26]],"date-time":"2021-02-26T02:02:45Z","timestamp":1614304965000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":10,"title":["Ready,\n                    <tt>Set<\/tt>\n                    , Verify! Applying\n                    <tt>hs-to-coq<\/tt>\n                    to real-world Haskell code"],"prefix":"10.1017","volume":"31","author":[{"given":"JOACHIM","family":"BREITNER","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7590-5291","authenticated-orcid":false,"given":"ANTAL","family":"SPECTOR-ZABUSKY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8720-883X","authenticated-orcid":false,"given":"YAO","family":"LI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"CHRISTINE","family":"RIZKALLAH","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JOHN","family":"WIEGLEY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JOSHUA","family":"COHEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"STEPHANIE","family":"WEIRICH","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2021,2,26]]},"reference":[{"key":"S0956796820000283_ref24","unstructured":"Joseph, A. M. (2014) Generalized arrows. Ph.D. thesis, EECS Department, University of California, Berkeley."},{"key":"S0956796820000283_ref15","first-page":"1","volume-title":"Workshop on Programming Languages and Operating Systems (PLOS)","author":"Chen","year":"2017"},{"key":"S0956796820000283_ref29","unstructured":"Letouzey, P. (2002) A new extraction for Coq. In TYPES. LNCS, vol. 2646. Springer, pp. 200\u2013219."},{"key":"S0956796820000283_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000104"},{"key":"S0956796820000283_ref30","unstructured":"Licata, D. (2012) 15\u2013150 Lecture 21: Red-black trees. Lecture at the Oregon Programming Language Summer School."},{"key":"S0956796820000283_ref35","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000282"},{"key":"S0956796820000283_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_26"},{"key":"S0956796820000283_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"S0956796820000283_ref42","unstructured":"Okasaki, C. & Gill, A. (1998) Fast mergeable integer maps. In Workshop on ML, pp. 77\u201386."},{"key":"S0956796820000283_ref16","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1145\/351240.351266","volume-title":"ICFP","author":"Claessen","year":"2000"},{"key":"S0956796820000283_ref38","unstructured":"Nipkow, T. & Dirix, S. (2018) Weight-balanced trees. In Archive of Formal Proofs, http:\/\/isa-afp.org\/entries\/Weight_Balanced_Trees.html, Formal proof development."},{"key":"S0956796820000283_ref51","first-page":"269","volume-title":"ICFP","author":"Vazou","year":"2014"},{"key":"S0956796820000283_ref53","first-page":"1","article-title":"Refinement reflection: Complete verification with SMT","volume":"2","author":"Vazou","year":"2018","journal-title":"PACMPL"},{"key":"S0956796820000283_ref52","first-page":"63","volume-title":"Haskell Symposium","author":"Vazou","year":"2017"},{"key":"S0956796820000283_ref5","unstructured":"Appel, A. W. (2011) Efficient Verified Red-Black Trees."},{"key":"S0956796820000283_ref10","unstructured":"Brady, E. (2017) Type-driven development with Idris. Manning."},{"key":"S0956796820000283_ref17","unstructured":"Coquand, T. (1989) Metamathematical investigations of a calculus of constructions. Tech. rept. RR-1088. INRIA."},{"key":"S0956796820000283_ref37","first-page":"307","article-title":"Automatic functional correctness proofs for functional search trees","volume":"9807","author":"Nipkow","year":"2016","journal-title":"Interactive Theorem Proving (ITP) 2016"},{"key":"S0956796820000283_ref41","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104"},{"key":"S0956796820000283_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_20"},{"key":"S0956796820000283_ref55","unstructured":"Wiegley, J. (2017) coq-haskell: A Library for Formalizing Haskell Types and Functions in Coq. https:\/\/github.com\/jwiegley\/coq-haskell."},{"key":"S0956796820000283_ref43","unstructured":"Peyton Jones, S. , Tolmach, A. & Hoare, T. (2001) Playing by the rules: rewriting as a practical optimisation technique in GHC. In Haskell Workshop."},{"key":"S0956796820000283_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"S0956796820000283_ref19","first-page":"60","volume-title":"Haskell Symposium","author":"Derrin","year":"2006"},{"key":"S0956796820000283_ref4","unstructured":"Anand, A. , Appel, A. , Morrisett, G. , Paraskevopoulou, Z. , Pollack, R. , Savary Belanger, O. , Sozeau, M. & Weaver, M. (2017) CertiCoq: A verified compiler for Coq. In CoqPL Workshop, CoqPL 2017."},{"key":"S0956796820000283_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489838"},{"key":"S0956796820000283_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1637837.1637848"},{"key":"S0956796820000283_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"S0956796820000283_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628163"},{"key":"S0956796820000283_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"S0956796820000283_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"S0956796820000283_ref11","unstructured":"Campbell, T. (2010) Bug in Data.Map. e-mail to the Haskell libraries mailing list."},{"key":"S0956796820000283_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088355"},{"key":"S0956796820000283_ref27","unstructured":"Kr\u00f6ning, D. , R\u00fcmmer, P. & Weissenbacher, G. (2009) A proposal for a theory of finite sets, lists, and maps for the SMT-Lib standard. In Informal Proceedings, 7th International Workshop on Satisfiability Modulo Theories at CADE, vol. 22."},{"key":"S0956796820000283_ref31","unstructured":"The, Coq development team. (2016) The Coq proof assistant reference manual. LogiCal Project. Version 8.6.1."},{"key":"S0956796820000283_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3167089"},{"key":"S0956796820000283_ref47","unstructured":"Spector-Zabusky, A. , Breitner, J. , Rizkallah, C. & Weirich, S. (2018) Total Haskell is reasonable Coq. In CPP. ACM, pp. 14\u201327."},{"key":"S0956796820000283_ref6","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2016.0331"},{"key":"S0956796820000283_ref7","unstructured":"Besson, F. (2006) Fast reflexive arithmetic tactics: the linear case and beyond. In TYPES. Lecture Notes in Computer Science, vol. 4502. Springer, pp. 48\u201362."},{"key":"S0956796820000283_ref48","doi-asserted-by":"crossref","unstructured":"Straka, M. (2010) The performance of the Haskell containers package. Proceedings of the Third ACM Haskell Symposium on Haskell, Haskell 2010. New York, NY, USA: ACM, pp. 13\u201324.","DOI":"10.1145\/1863523.1863526"},{"key":"S0956796820000283_ref22","unstructured":"Hallgren, T. , Hook, J. , Jones, M. P. & Kieburtz, R. B. (2004) An overview of the Programatica toolset. In HCSS."},{"key":"S0956796820000283_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0956796820000283_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2004.07.002"},{"key":"S0956796820000283_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_48"},{"key":"S0956796820000283_ref13","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A. (2010b) Program verification through characteristic formulae. In ICFP. ACM, pp. 321\u2013332.","DOI":"10.1145\/1932681.1863590"},{"key":"S0956796820000283_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"S0956796820000283_ref33","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1145\/321479.321481","article-title":"PATRICIA\u2014Practical Algorithm To Retrieve Information Coded in Alphanumeric","volume":"15","author":"Morrison","year":"1968","journal-title":"J. ACM"},{"key":"S0956796820000283_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"S0956796820000283_ref2","author":"Adams","year":"1992"},{"key":"S0956796820000283_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/800152.804906"},{"key":"S0956796820000283_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"S0956796820000283_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_15"},{"key":"S0956796820000283_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"S0956796820000283_ref9","unstructured":"Bove, A. , Dybjer, P. & Norell, U. (2009) A brief overview of Agda \u2013 A functional language with dependent types. In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Berghofer, S. , Nipkow, T. , Urban, C. & Wenzel, M. (eds), Lecture Notes in Computer Science, vol. 5674. Springer."},{"key":"S0956796820000283_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951940"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796820000283","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:54Z","timestamp":1779835014000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796820000283\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":55,"alternative-id":["S0956796820000283"],"URL":"https:\/\/doi.org\/10.1017\/s0956796820000283","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}],"article-number":"e5"}}