{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:58:19Z","timestamp":1760785099042,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"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":[[2022,10,31]]},"abstract":"<jats:p>Program equivalence checking is the task of confirming that two programs have the same behavior on corresponding inputs. We develop a calculus based on symbolic execution and coinduction to check the equivalence of programs in a non-strict functional language. Additionally, we show that our calculus can be used to derive counterexamples for pairs of inequivalent programs, including counterexamples that arise from non-termination. We describe a fully automated approach for finding both equivalence proofs and counterexamples. Our implementation, Nebula, proves equivalences of programs written in Haskell. We demonstrate Nebula's practical effectiveness at both proving equivalence and producing counterexamples automatically by applying Nebula to existing benchmark properties.<\/jats:p>","DOI":"10.1145\/3563340","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1469-1496","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Checking equivalence in a non-strict language"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6084-2387","authenticated-orcid":false,"given":"John C.","family":"Kolesar","sequence":"first","affiliation":[{"name":"Yale University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-0776","authenticated-orcid":false,"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4925-3861","authenticated-orcid":false,"given":"William T.","family":"Hallahan","sequence":"additional","affiliation":[{"name":"Binghamton University, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"e_1_2_1_2_1","unstructured":"Joachim Breitner. 2018. hs-to-coq supports coinduction. https:\/\/mobile.twitter.com\/nomeata\/status\/977257104120664064 \t\t\t\t  Joachim Breitner. 2018. hs-to-coq supports coinduction. https:\/\/mobile.twitter.com\/nomeata\/status\/977257104120664064"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236784"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.87"},{"key":"e_1_2_1_6_1","volume-title":"Avenir: Managing Data Plane Diversity with Control Plane Synthesis. In NSDI. 133\u2013153.","author":"Campbell Eric Hayden","year":"2021","unstructured":"Eric Hayden Campbell , William T. Hallahan , Priya Srikumar , Carmelo Cascone , Jed Liu , Vignesh Ramamurthy , Hossein Hojjat , Ruzica Piskac , Robert Soul\u00e9 , and Nate Foster . 2021 . Avenir: Managing Data Plane Diversity with Control Plane Synthesis. In NSDI. 133\u2013153. Eric Hayden Campbell, William T. Hallahan, Priya Srikumar, Carmelo Cascone, Jed Liu, Vignesh Ramamurthy, Hossein Hojjat, Ruzica Piskac, Robert Soul\u00e9, and Nate Foster. 2021. Avenir: Managing Data Plane Diversity with Control Plane Synthesis. In NSDI. 133\u2013153."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22655-7_28"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.29007\/3qwr"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987597"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_22"},{"key":"e_1_2_1_12_1","unstructured":"Conal Elliot. 2010. Non-strict memoization. http:\/\/conal.net\/blog\/posts\/nonstrict-memoization \t\t\t\t  Conal Elliot. 2010. Non-strict memoization. http:\/\/conal.net\/blog\/posts\/nonstrict-memoization"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354175"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804303"},{"key":"e_1_2_1_15_1","first-page":"353","article-title":"Proof methods for corecursive programs","volume":"66","author":"Gibbons Jeremy","year":"2005","unstructured":"Jeremy Gibbons and Graham Hutton . 2005 . Proof methods for corecursive programs . Fundamenta Informaticae , 66 , 4 (2005), 353 \u2013 366 . https:\/\/dl.acm.org\/doi\/abs\/10.5555\/1227189.1227192 Jeremy Gibbons and Graham Hutton. 2005. Proof methods for corecursive programs. Fundamenta Informaticae, 66, 4 (2005), 353\u2013366. https:\/\/dl.acm.org\/doi\/abs\/10.5555\/1227189.1227192","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3573-9_6"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314618"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_21"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398857.2384648"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7083308"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000493"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428257"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_27"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73859-6_25"},{"key":"e_1_2_1_28_1","volume-title":"Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell. In Haskell Symposium. https:\/\/nikivazou.github.io\/static\/Haskell22\/coinduction.pdf","author":"Mastorou Lykourgos","year":"2022","unstructured":"Lykourgos Mastorou , Nikolaos Papaspyrou , and Niki Vazou . 2022 . Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell. In Haskell Symposium. https:\/\/nikivazou.github.io\/static\/Haskell22\/coinduction.pdf Lykourgos Mastorou, Nikolaos Papaspyrou, and Niki Vazou. 2022. Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell. In Haskell Symposium. https:\/\/nikivazou.github.io\/static\/Haskell22\/coinduction.pdf"},{"key":"e_1_2_1_29_1","unstructured":"Dragana Milovancevic Julie Giunta and Viktor Kuncak. 2021. On Proving and Disproving Equivalence of Functional Programming Assignments. \t\t\t\t  Dragana Milovancevic Julie Giunta and Viktor Kuncak. 2021. On Proving and Disproving Equivalence of Functional Programming Assignments."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314643"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737971"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_2_1_33_1","volume-title":"Haskell workshop. 1, 203\u2013233","author":"Jones Simon Peyton","year":"2001","unstructured":"Simon Peyton Jones , Andrew Tolmach , and Tony Hoare . 2001 . Playing by the rules: rewriting as a practical optimisation technique in GHC . In Haskell workshop. 1, 203\u2013233 . Simon Peyton Jones, Andrew Tolmach, and Tony Hoare. 2001. Playing by the rules: rewriting as a practical optimisation technique in GHC. In Haskell workshop. 1, 203\u2013233."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61055-3_27"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03741-2_10"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516510"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.17"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2490301.2451150"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_20"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_2"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_28"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563340","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563340"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":42,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563340"],"URL":"https:\/\/doi.org\/10.1145\/3563340","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}