{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T21:09:39Z","timestamp":1770239379641,"version":"3.49.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1911149,1943623"],"award-info":[{"award-number":["1911149,1943623"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,8,15]]},"abstract":"<jats:p>\n                    The problem of automatically proving the equality of terms over recursive functions and inductive data types is challenging, as such proofs often require auxiliary lemmas which must themselves be proven. Previous attempts at lemma discovery compromise on either efficiency or efficacy.\n                    <jats:italic toggle=\"yes\">Goal-directed<\/jats:italic>\n                    approaches are fast but limited in expressiveness, as they can only discover auxiliary lemmas which entail their goals. Theory exploration approaches are expressive but inefficient, as they exhaustively enumerate candidate lemmas.\n                  <\/jats:p>\n                  <jats:p>\n                    We introduce\n                    <jats:italic toggle=\"yes\">e-graph guided lemma discovery<\/jats:italic>\n                    , a new approach to finding equational proofs that makes theory exploration goal-directed. We accomplish this by using e-graphs and equality saturation to efficiently construct and compactly represent the space of all goal-oriented proofs. This allows us to explore only those auxiliary lemmas\n                    <jats:italic toggle=\"yes\">guaranteed<\/jats:italic>\n                    to help make progress on some of these proofs. We implemented our method in a new prover called\n                    <jats:sc>CCLemma<\/jats:sc>\n                    and compared it with three state-of-the-art provers across a variety of benchmarks.\n                    <jats:sc>CCLemma<\/jats:sc>\n                    performs consistently well on two standard benchmarks and additionally solves 50% more problems than the next best tool on a new challenging set.\n                  <\/jats:p>","DOI":"10.1145\/3674653","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"818-844","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6699-0430","authenticated-orcid":false,"given":"Cole","family":"Kurashige","sequence":"first","affiliation":[{"name":"University of California, San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0150-8629","authenticated-orcid":false,"given":"Ruyi","family":"Ji","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7212-0714","authenticated-orcid":false,"given":"Aditya","family":"Giridharan","sequence":"additional","affiliation":[{"name":"University of California, San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-8249-7699","authenticated-orcid":false,"given":"Mark","family":"Barbone","sequence":"additional","affiliation":[{"name":"University of California, San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7504-2009","authenticated-orcid":false,"given":"Daniel","family":"Noor","sequence":"additional","affiliation":[{"name":"Technion, Haifa, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7276-7644","authenticated-orcid":false,"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[{"name":"Technion, Haifa, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California, San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5571-173X","authenticated-orcid":false,"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[{"name":"University of California, San Diego, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.122"},{"key":"e_1_3_1_3_1","unstructured":"Richard S. Bird and Oege de Moor. 1997. Algebra of programming. Prentice Hall."},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_10"},{"key":"e_1_3_1_6_1","doi-asserted-by":"crossref","unstructured":"Leonardo Mendonca de de and Nikolaj Bjorner. 2007. Efficient E-Matching for SMT Solvers. In CADE (Lecture Notes in Computer Science Vol. 4603). Springer 183\u2013198.","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_22"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_7"},{"key":"e_1_3_1_9_1","article-title":"On Automated Lemma Generation for Separation Logic with Inductive Definitions","author":"Enea Constantin","year":"2015","unstructured":"Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. 2015. On Automated Lemma Generation for Separation Logic with Inductive Definitions. arXiv:1507.05581 [cs.LO]","journal-title":"arXiv:1507.05581 [cs.LO]"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan Danya Lette Victor Nicolet. 2022. Recursion synthesis with unrealizability witnesses. In PLDI \u201922: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation San Diego CA USA June 13 - 17 2022 Ranjit Jhala and Isil Dillig (Eds.). ACM 244\u2013259. https:\/\/10.1145\/3519939.3523726 10.1145\/3519939.3523726","DOI":"10.1145\/3519939.3523726"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Andrew John Gill John Launchbury and Simon L. Peyton Jones. 1993. A Short Cut to Deforestation. In Proceedings of the conference on Functional programming languages and computer architecture FPCA 1993 Copenhagen Denmark June 9-11 1993 John Williams (Ed.). ACM 223\u2013232. https:\/\/doi.org\/10.1145\/165180.165214 10.1145\/165180.165214","DOI":"10.1145\/165180.165214"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_34"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_27"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Zhenjiang Hu Hideya Iwasaki Masato Takeichi and Akihiko Takano. 1997. Tupling Calculation Eliminates Multiple Data Traversals. In Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP \u201897) Amsterdam The Netherlands June 9-11 1997 Simon L. Peyton Jones Mads Tofte and A. Michael Berman (Eds.). ACM 164\u2013175. https:\/\/doi.org\/10.1145\/258948.258964 10.1145\/258948.258964","DOI":"10.1145\/258948.258964"},{"key":"e_1_3_1_16_1","unstructured":"Idris Team. 2024. Idris 2. https:\/\/www.idrislang.org\/index.html"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Andrew Ireland and Alan Bundy. 1996. Productive Use of Failure in Inductive Proof. Springer Netherlands Dordrecht 79\u2013111. https:\/\/doi.org\/10.1007\/978-94-009-1675-3_3 10.1007\/978-94-009-1675-3_3","DOI":"10.1007\/978-94-009-1675-3_3"},{"key":"e_1_3_1_18_1","unstructured":"Ruyi Ji Yuwei Zhao Yingfei Xiong Di Wang Lu Zhang and Zhenjiang Hu. 2024. Decomposition-Based Synthesis for Applying Divide-and-Conquer-Like Algorithmic Paradigms. arXiv:2202.12193 [cs.PL]"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-23250-4_9"},{"key":"e_1_3_1_20_1","unstructured":"Eddie Jones C-.H. Luke Ong and Steven Ramsay. 2021. CycleQ: An Efficient Basis for Cyclic Equational Reasoning. CoRR abs\/2111.12553 (2021). arXiv:2111.12553 http:\/\/arxiv.org\/abs\/2111.12553"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Cole Kurashige Ruyi Ji Aditya Giridharan Mark Barbone Daniel Noor Shachar Itzhaky Ranjit Jhala and Nadia Polikarpova. 2024. CCLemma : E-Graph Guided Lemma Discovery for Inductive Equational Proofs. https:\/\/doi.org\/10.5281\/Zenodo.11508050 10.5281\/Zenodo.11508050","DOI":"10.5281\/Zenodo.11508050"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563354"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Yutaka Nagashima. 2021. Faster Smarter Proof by Induction in Isabelle\/HOL. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence IJCAI 2021 Virtual Event \/ Montreal Canada 19-27 August 2021 Zhi-Hua Zhou (Ed.). ijcai.org 1981\u20131988. https:\/\/doi.org\/10.24963\/IJCAI.2021\/273 10.24963\/IJCAI.2021\/273","DOI":"10.24963\/IJCAI.2021\/273"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-42441-0_9"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"Chandrakana Nandi Max Willsey Amy Zhu Yisu Remy Wang Brett Saiki Adam Anderson Adriana Schulz Dan Grossman and Zachary Tatlock. 2021. Rewrite Rule Inference Using Equality Saturation. Proc. ACM Program. Lang. 5 OOPSLA Article 119 (oct 2021) 28 pages. https:\/\/doi.org\/10.1145\/3485496 10.1145\/3485496","DOI":"10.1145\/3485496"},{"key":"e_1_3_1_28_1","doi-asserted-by":"crossref","unstructured":"Greg Nelson and Derek C. Oppen. 1980. Fast Decision Procedures Based on Congruence Closure. J. ACM 27 2 (1980) 356\u2013364.","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_1_29_1","unstructured":"Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph. D. Dissertation. Department of Computer Science and Engineering Chalmers University of Technology SE-412 96 G\u00f6teborg Sweden."},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_28"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018623"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_6"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563306"},{"key":"e_1_3_1_36_1","doi-asserted-by":"crossref","unstructured":"William Sonnex Sophia Drossopoulou and Susan Eisenbach. 2012. Zeno: An Automated Prover for Properties of Recursive Data Structures. In TACAS.","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158097"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19027-9_23"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_35"},{"key":"e_1_3_1_42_1","unstructured":"Yichen Yang Phitchaya Phothilimthana Yisu Wang Max Willsey Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. In Proceedings of Machine Learning and Systems A. Smola A. Dimakis and I. Stoica (Eds.) Vol. 3. 255\u2013268. https:\/\/proceedings.mlsys.org\/paper\/2021\/file\/65ded5353c5ee48d0b7d48c591b8f430-Paper.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674653","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674653","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:50:05Z","timestamp":1770191405000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674653"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":41,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674653"],"URL":"https:\/\/doi.org\/10.1145\/3674653","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}