{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:36:14Z","timestamp":1758054974308,"version":"3.44.0"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"unspecified","delay-in-days":257,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <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, <jats:sc>nebula<\/jats:sc>, proves equivalences of programs written in Haskell. We demonstrate <jats:sc>nebula<\/jats:sc>\u2019s practical effectiveness at both proving equivalence and producing counterexamples automatically by applying <jats:sc>nebula<\/jats:sc> to existing benchmark properties.<\/jats:p>","DOI":"10.1017\/s0956796825100099","type":"journal-article","created":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T05:36:38Z","timestamp":1757914598000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Checking equivalence in a non-strict language"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6084-2387","authenticated-orcid":false,"given":"JOHN CHARLES","family":"KOLESAR","sequence":"first","affiliation":[{"name":"Yale University"}]},{"given":"RUZICA","family":"PISKAC","sequence":"additional","affiliation":[{"name":"Yale University"}]},{"given":"WILLIAM TRIEST","family":"HALLAHAN","sequence":"additional","affiliation":[{"name":"Binghamton University"}]}],"member":"56","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"S0956796825100099_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"S0956796825100099_ref38","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1145\/2813885.2737971","article-title":"Relatively complete counterexamples for higher-order programs","volume":"50","author":"Van Horn","year":"2015","journal-title":"ACM SIGPLAN Not."},{"key":"S0956796825100099_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45788-7_13"},{"key":"S0956796825100099_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314643"},{"key":"S0956796825100099_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804303"},{"key":"S0956796825100099_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/11554554_8"},{"key":"S0956796825100099_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"S0956796825100099_ref22","first-page":"353","article-title":"Proof methods for corecursive programs","volume":"66","author":"Gibbons","year":"2005","journal-title":"Fundam. Inf."},{"key":"S0956796825100099_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03741-2_10"},{"key":"S0956796825100099_ref7","unstructured":"Breitner, J. (2018) hs-to-coq supports coinduction. Available at: https:\/\/mobile.twitter.com\/nomeata\/status\/977257104120664064."},{"key":"S0956796825100099_ref13","first-page":"609","volume-title":"European Conference on Object-Oriented Programming","author":"Carbin","year":"2011"},{"key":"S0956796825100099_ref41","doi-asserted-by":"crossref","unstructured":"Peyton Jones, S. L. (1996) Compiling haskell by program transformation: A report from the trenches. In European Symposium on Programming. Springer, pp. 18\u201344.","DOI":"10.1007\/3-540-61055-3_27"},{"key":"S0956796825100099_ref14","first-page":"16","volume-title":"ATx\/WInG@ IJCAR","author":"Claessen","year":"2012"},{"key":"S0956796825100099_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/2490301.2451150"},{"key":"S0956796825100099_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111056"},{"key":"S0956796825100099_ref32","first-page":"382","volume-title":"International Symposium on Formal Methods","author":"Leino","year":"2014"},{"key":"S0956796825100099_ref19","unstructured":"Elliott, C. (2010) Non-strict memoization. Available at: http:\/\/conal.net\/blog\/posts\/nonstrict-memoization."},{"key":"S0956796825100099_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"S0956796825100099_ref18","first-page":"279","volume-title":"International Conference on Automated Deduction","author":"Dixon","year":"2003"},{"key":"S0956796825100099_ref4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S1571-0661(04)00265-8","article-title":"Evaluation strategies for functional logic programming","volume":"57","author":"Antoy","year":"2001","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"S0956796825100099_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_20"},{"key":"S0956796825100099_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002303"},{"key":"S0956796825100099_ref35","doi-asserted-by":"crossref","unstructured":"Mastorou, L. , Papaspyrou, N. & Vazou, N. (2022) Coinduction inductively: Mechanizing coinductive proofs in liquid haskell. Haskell Symposium.10.1145\/3554303","DOI":"10.1145\/3554303"},{"key":"S0956796825100099_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000493"},{"key":"S0956796825100099_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"S0956796825100099_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2398857.2384648"},{"key":"S0956796825100099_ref44","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1516507.1516510","article-title":"On the origins of bisimulation and coinduction","volume":"31","author":"Sangiorgi","year":"2009","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)."},{"key":"S0956796825100099_ref26","first-page":"291","volume-title":"International Conference on Interactive Theorem Proving","author":"Johansson","year":"2010"},{"key":"S0956796825100099_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3236784"},{"key":"S0956796825100099_ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.87"},{"key":"S0956796825100099_ref36","unstructured":"Milovancevic, D. , Giunta, J. & Kuncak, V. (2021) On Proving and Disproving Equivalence of Functional Programming Assignments. Technical report."},{"key":"S0956796825100099_ref52","doi-asserted-by":"crossref","unstructured":"Vidal, G. (2015) Towards symbolic execution in erlang. In Perspectives of System Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24\u201327, 2014. Revised Selected Papers 9. Springer, pp. 351\u2013360.10.1007\/978-3-662-46823-4_28","DOI":"10.1007\/978-3-662-46823-4_28"},{"key":"S0956796825100099_ref12","unstructured":"Campbell, E. H. , Hallahan, W. T. , Srikumar, P. , Cascone, C. , Liu, J. , Ramamurthy, V. , Hojjat, H. , Piskac, R. , Soul\u00e9, R. & Foster, N. (2021) Avenir: Managing data plane diversity with control plane synthesis. In NSDI, pp. 133\u2013153."},{"key":"S0956796825100099_ref49","first-page":"407","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Sonnex","year":"2012"},{"key":"S0956796825100099_ref50","doi-asserted-by":"crossref","unstructured":"Spector-Zabusky, A. , Breitner, J. , Rizkallah, C. & Weirich, S. (2018) Total haskell is reasonable coq. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 14\u201327.10.1145\/3167092","DOI":"10.1145\/3167092"},{"key":"S0956796825100099_ref5","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/1721654.1721675","article-title":"Functional logic programming","volume":"53","author":"Antoy","year":"2010","journal-title":"Commun. ACM."},{"key":"S0956796825100099_ref15","first-page":"392","volume-title":"International Conference on Automated Deduction","author":"Claessen","year":"2013"},{"key":"S0956796825100099_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"S0956796825100099_ref23","doi-asserted-by":"crossref","unstructured":"Gordon, A. D. (1995) A tutorial on co-induction and functional programming. In Functional Programming, Glasgow 1994, pp. 78\u201395.10.1007\/978-1-4471-3573-9_6","DOI":"10.1007\/978-1-4471-3573-9_6"},{"key":"S0956796825100099_ref45","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.17"},{"key":"S0956796825100099_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_2"},{"key":"S0956796825100099_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3428257"},{"key":"S0956796825100099_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314618"},{"key":"S0956796825100099_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354175"},{"key":"S0956796825100099_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"S0956796825100099_ref2","doi-asserted-by":"crossref","unstructured":"Alpuente, M. , Falaschi, M. & Vidal, G. (1996) Narrowing-driven partial evaluation of functional logic programs. In Programming Languages and Systems\u2013ESOP\u201996: 6th European Symposium on Programming Link\u00f6ping, Sweden, April 22\u201324, 1996 Proceedings 6. Springer, pp. 45\u201361.10.1007\/3-540-61055-3_28","DOI":"10.1007\/3-540-61055-3_28"},{"key":"S0956796825100099_ref40","unstructured":"Peyton Jones, S. , Tolmach, A. & Hoare, T. (2001) Playing by the rules: rewriting as a practical optimisation technique in ghc. In Haskell Workshop, pp. 203\u2013233."},{"key":"S0956796825100099_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0956796825100099_ref16","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987597"},{"key":"S0956796825100099_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"S0956796825100099_ref1","unstructured":"AbdelGawad, M. A. (2019) Induction, coinduction, and fixed points: Intuitions and tutorial. arXiv preprint arXiv:1903.05127."},{"key":"S0956796825100099_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73859-6_25"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796825100099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T05:36:43Z","timestamp":1757914603000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796825100099\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":52,"alternative-id":["S0956796825100099"],"URL":"https:\/\/doi.org\/10.1017\/s0956796825100099","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e19"}}