{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T22:49:12Z","timestamp":1774392552034,"version":"3.50.1"},"reference-count":121,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"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":["1752814,FW-HTF 2129008,CA-HDR 2033558"],"award-info":[{"award-number":["1752814,FW-HTF 2129008,CA-HDR 2033558"]}],"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,6,20]]},"abstract":"<jats:p>\n            We present an enumerative program synthesis framework called\n            <jats:italic toggle=\"yes\">component-based refactoring<\/jats:italic>\n            that can refactor \u201cdirect\u201d style code that does not use library components into equivalent \u201ccombinator\u201d style code that does use library components. This framework introduces a sound but incomplete technique to check the equivalence of direct code and combinator code called\n            <jats:italic toggle=\"yes\">equivalence by canonicalization<\/jats:italic>\n            that does not rely on input-output examples or logical specifications. Moreover, our approach can repurpose existing compiler optimizations, leveraging decades of research from the programming languages community. We instantiated our new synthesis framework in two contexts: (i) higher-order functional combinators such as\n            <jats:monospace>map<\/jats:monospace>\n            and\n            <jats:monospace>filter<\/jats:monospace>\n            in the staticallytyped functional programming language Elm and (ii) high-performance numerical computing combinators provided by the NumPy library for Python. We implemented both instantiations in a tool called\n            <jats:sc>Cobbler<\/jats:sc>\n            and evaluated it on thousands of real programs to test the performance of the component-based refactoring framework in terms of execution time and output quality. Our work offers evidence that synthesis-backed refactoring can apply across a range of domains without specification beyond the input program.\n          <\/jats:p>","DOI":"10.1145\/3656453","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1879-1904","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Equivalence by Canonicalization for Synthesis-Backed Refactoring"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2311-1873","authenticated-orcid":false,"given":"Justin","family":"Lubin","sequence":"first","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7778-5043","authenticated-orcid":false,"given":"Jeremy","family":"Ferguson","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3618-0966","authenticated-orcid":false,"given":"Kevin","family":"Ye","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6174-2644","authenticated-orcid":false,"given":"Jacob","family":"Yim","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0557-3580","authenticated-orcid":false,"given":"Sarah E.","family":"Chasins","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"M. B. S. Ahmad J. Ragan-Kelley A. Cheung and S. Kamil. 2019. Automatically Translating Image Processing Libraries to Halide. In TOG. https:\/\/doi.org\/10.1145\/3355089.3356549 10.1145\/3355089.3356549","DOI":"10.1145\/3355089.3356549"},{"key":"e_1_3_2_3_2","volume-title":"Calibrating Research in Program Synthesis Using 72,000 Hours of Programmer Time","author":"Akiba T.","year":"2013","unstructured":"T. Akiba, K. Imajo, H. Iwami, Y. Iwata, T. Kataoka, N. Takahashi, M. Moskal, and N. Swamy. 2013. Calibrating Research in Program Synthesis Using 72,000 Hours of Programmer Time. Technical Report. Microsoft Research."},{"key":"e_1_3_2_4_2","doi-asserted-by":"crossref","unstructured":"A. Albarghouthi S. Gulwani and Z. Kincaid. 2013. Recursive Program Synthesis. In CAV.","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_3_2_5_2","unstructured":"F. E. Allen and J. Cocke. 1971. A Catalogue of Optimizing Transformations."},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","unstructured":"R. Alur P. \u010cern\u00fd and A. Radhakrishna. 2015. Synthesis Through Unification. In CAV.","DOI":"10.1007\/978-3-319-21668-3_10"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"R. Alur A. Radhakrishna and A. Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In TACAS. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18 10.1007\/978-3-662-54577-5_18","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"T. Antonopoulos E. Koskinen T. C. Le R. Nagasamudram D. A. Naumann and M. Ngo. 2023. An Algebra of Alignment for Relational Verification. In POPL. https:\/\/doi.org\/10.1145\/3571213 10.1145\/3571213","DOI":"10.1145\/3571213"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/909332"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"S. Bansal and A. Aiken. 2006. Automatic Generation of Peephole Superoptimizers. In OSR.","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"S. Barke H. Peleg and N. Polikarpova. 2020. Just-in-Time Learning for Bottom-up Enumerative Synthesis. In OOPSLA. https:\/\/doi.org\/10.1145\/3428295 10.1145\/3428295","DOI":"10.1145\/3428295"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"G. Barthe J. Manuel Crespo and C. Kunz. 2011. Relational Verification Using Product Programs. In FM. https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17 10.1007\/978-3-642-21437-0_17","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_2_13_2","doi-asserted-by":"crossref","unstructured":"G. Barthe J. Manuel Crespo and C. Kunz. 2016. Product Programs and Relational Program Logics. In JLAMP.","DOI":"10.1016\/j.jlamp.2016.05.004"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"G. Barthe B. Gr\u00e9goire and S. Zanella B\u00e9guelin. 2009. Formal Certification of Code-Based Cryptographic Proofs. In POPL. https:\/\/doi.org\/10.1145\/1480881.1480894 10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"R. Bavishi C. Lemieux R. Fox K. Sen and I. Stoica. 2019. AutoPandas: Neural-Backed Generators for Program Synthesis. In OOPSLA. https:\/\/doi.org\/10.1145\/3360594 10.1145\/3360594","DOI":"10.1145\/3360594"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"N. Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In POPL. https:\/\/doi.org\/10.1145\/964001.964003 10.1145\/964001.964003","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"U. Berger and H. Schwichtenberg. 1991. An Inverse of the Evaluation Functional for Typed Lambda-Calculus. In LICS. https:\/\/doi.org\/10.1109\/LICS.1991.151645 10.1109\/LICS.1991.151645","DOI":"10.1109\/LICS.1991.151645"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"A. J. Bernstein. 1966. Analysis of Programs for Parallel Processing. In Transactions on Electronic Computers. https:\/\/doi.org\/10.1109\/PGEC.1966.264565 10.1109\/PGEC.1966.264565","DOI":"10.1109\/PGEC.1966.264565"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"S. Bhatia S. Kohli S. A. Seshia and A. Cheung. 2023. Building Code Transpilers for Domain-Specific Languages Using Program Synthesis. In ECOOP. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2023.38 10.4230\/LIPIcs.ECOOP.2023.38","DOI":"10.4230\/LIPIcs.ECOOP.2023.38"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"A. Biere A. Cimatti E. Clarke and Y. Zhu. 1999. Symbolic Model Checking without BDDs. In TACAS. https:\/\/doi.org\/10.1007\/3-540-49059-0_14 10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","unstructured":"R. Bird and O. de Moor. 1997. Algebra of Programming.","DOI":"10.1007\/978-3-642-61455-2_12"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"H. Botelho Guerra J. F. Ferreira and J. Costa Seco. 2023. Hoogle\u22c6: Constants and \u03bb-Abstractions in Petri-net-based Synthesis Using Symbolic Execution. In ECOOP. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2023.4 10.4230\/LIPIcs.ECOOP.2023.4","DOI":"10.4230\/LIPIcs.ECOOP.2023.4"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"M. Bowers T. X. Olausson L. Wong G. Grand J. B. Tenenbaum K. Ellis and A. Solar-Lezama. 2023. Top-Down Synthesis for Library Learning. In POPL. https:\/\/doi.org\/10.1145\/3571234 10.1145\/3571234","DOI":"10.1145\/3571234"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"M. Burke and R. Cytron. 1986. Interprocedural Dependence Analysis and Parallelization. In CC. https:\/\/doi.org\/10.1145\/12276.13328 10.1145\/12276.13328","DOI":"10.1145\/12276.13328"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"D. Cao R. Kunkel C. Nandi M. Willsey Z. Tatlock and N. Polikarpova. 2023. babble: Learning Better Abstractions with E-Graphs and Anti-unification. In POPL. https:\/\/doi.org\/10.1145\/3571207 10.1145\/3571207","DOI":"10.1145\/3571207"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"J. Chen J. Wei Y. Feng O. Bastani and I. Dillig. 2019. Relational Verification Using Reinforcement Learning. In OOPSLA. https:\/\/doi.org\/10.1145\/3360567 10.1145\/3360567","DOI":"10.1145\/3360567"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"A. Cheung A. Solar-Lezama and S. Madden. 2013. Optimizing Database-Backed Applications with Query Synthesis. In PLDI. https:\/\/doi.org\/10.1145\/2491956.2462180 10.1145\/2491956.2462180","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"B. Churchill O. Padon R. Sharma and A. Aiken. 2019. Semantic Program Alignment for Equivalence Checking. In PLDI. https:\/\/doi.org\/10.1145\/3314221.3314596 10.1145\/3314221.3314596","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","unstructured":"K. Claessen and J. Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In ICFP.","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"E. De Angelis F. Fioravanti A. Pettorossi and M. Proietti. 2014. VeriMAP: A Tool for Verifying Programs through Transformations. In TACAS. https:\/\/doi.org\/10.1007\/978-3-642-54862-8_47 10.1007\/978-3-642-54862-8_47","DOI":"10.1007\/978-3-642-54862-8_47"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"E. De Angelis F. Fioravanti A. Pettorossi and M. Proietti. 2016. Relational Verification Through Horn Clause Transformation. In SAS. https:\/\/doi.org\/10.1007\/978-3-662-53413-7_8 10.1007\/978-3-662-53413-7_8","DOI":"10.1007\/978-3-662-53413-7_8"},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","unstructured":"L. de Moura and N. Bj\u00f8rner. 2007. Efficient E-Matching for SMT Solvers. In CADE.","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"S. Dutta D. Sarkar A. Rawat and K. Singh. 2016. Validation of Loop Parallelization and Loop Vectorization Transformations. In ENASE. https:\/\/doi.org\/10.5220\/0005869501950202 10.5220\/0005869501950202","DOI":"10.5220\/0005869501950202"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"S. Eguchi N. Kobayashi and T. Tsukada. 2018. Automated Synthesis of Functional Programs with Auxiliary Functions. In APLAS. https:\/\/doi.org\/10.1007\/978-3-030-02768-1_13 10.1007\/978-3-030-02768-1_13","DOI":"10.1007\/978-3-030-02768-1_13"},{"key":"e_1_3_2_35_2","article-title":"Library Learning for Neurally-Guided Bayesian Program Induction","volume":"31","author":"Ellis K.","year":"2018","unstructured":"K. Ellis, L. Morales, M. Sabl\u00e9-Meyer, A. Solar-Lezama, and J. B. Tenenbaum. 2018. Library Learning for Neurally-Guided Bayesian Program Induction. In NeurIPS, Vol. 31.","journal-title":"NeurIPS"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","unstructured":"K. Ellis C. Wong M. Nye M. Sabl\u00e9-Meyer L. Morales L. Hewitt L. Cary A. Solar-Lezama and J. B. Tenenbaum. 2021. DreamCoder: Bootstrapping Inductive Program Synthesis with Wake-Sleep Library Learning. In PLDI.","DOI":"10.1145\/3453483.3454080"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"A. Farzan D. Lette and V. Nicolet. 2022. Recursion Synthesis with Unrealizability Witnesses. In PLDI. https:\/\/doi.org\/10.1145\/3519939.3523726 10.1145\/3519939.3523726","DOI":"10.1145\/3519939.3523726"},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","unstructured":"A. Farzan and V. Nicolet. 2021. Counterexample-Guided Partial Bounding for Recursive Function Synthesis. In CAV.","DOI":"10.1007\/978-3-030-81685-8_39"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"P. Feautrier. 1996. Automatic Parallelization in the Polytope Model. In The Data Parallel Programming Model. https:\/\/doi.org\/10.1007\/3-540-61736-1_44 10.1007\/3-540-61736-1_44","DOI":"10.1007\/3-540-61736-1_44"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Y. Feng R. Martins Y. Wang I. Dillig and T. W. Reps. 2017. Component-Based Synthesis for Complex APIs. In POPL. https:\/\/doi.org\/10.1145\/3009837.3009851 10.1145\/3009837.3009851","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"J. K. Feser S. Chaudhuri and I. Dillig. 2015. Synthesizing Data Structure Transformations from Input-Output Examples. In PLDI. https:\/\/doi.org\/10.1145\/2737924.2737977 10.1145\/2737924.2737977","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_2_42_2","unstructured":"Y. Futamura. 1971. Partial Evaluation of Computation Process\u2013An Approach to a Compiler-Compiler. In Systems Computers Controls."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"W. D. Goldfarb. 1981. The Undecidability of the Second-Order Unification Problem. In Theoretical Computer Science. https:\/\/doi.org\/10.1016\/0304-3975(81)90040-2 10.1016\/0304-3975(81)90040-2","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"P. Graf. 1995. Substitution Tree Indexing. In RTA. https:\/\/doi.org\/10.1007\/3-540-59200-8_52 10.1007\/3-540-59200-8_52","DOI":"10.1007\/3-540-59200-8_52"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","unstructured":"P. Graf and C. Meyer. 1996. Advanced Indexing Operations on Substitution Trees. In CADE.","DOI":"10.1007\/3-540-61511-3_113"},{"key":"e_1_3_2_46_2","doi-asserted-by":"crossref","unstructured":"S. Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-Output Examples. In POPL.","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Z. Guo M. James D. Justo J. Zhou Z. Wang R. Jhala and N. Polikarpova. 2019. Program Synthesis by Type-Guided Abstraction Refinement. In POPL. https:\/\/doi.org\/10.1145\/3371080 10.1145\/3371080","DOI":"10.1145\/3371080"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","unstructured":"M. Gupta S. Mukhopadhyay and N. Sinha. 2000. Automatic Parallelization of Recursive Procedures. In International Journal of Parallel Programming. https:\/\/doi.org\/10.1023\/A:1007560600904 10.1023\/A:1007560600904","DOI":"10.1023\/A:1007560600904"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"S. Gupta A. Saxena A. Mahajan and S. Bansal. 2018. Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition. In SAT. https:\/\/doi.org\/10.1007\/978-3-319-94144-8_22 10.1007\/978-3-319-94144-8_22","DOI":"10.1007\/978-3-319-94144-8_22"},{"key":"e_1_3_2_50_2","doi-asserted-by":"crossref","unstructured":"J. V. Guttag and J. J. Horning. 1978. The Algebraic Specification of Abstract Data Types. In Programming Methodology.","DOI":"10.1007\/978-1-4612-6315-9_21"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"C. R. Harris K. J. Millman S. J. van der Walt R. Gommers P. Virtanen D. Cournapeau E. Wieser J. Taylor S. Berg N. J. Smith et al. 2020. Array programming with NumPy. In Nature. https:\/\/doi.org\/10.1038\/s41586-020-2649-2 10.1038\/s41586-020-2649-2","DOI":"10.1038\/s41586-020-2649-2"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"M. Hofmann and E. Kitzelmann. 2010. I\/O Guided Detection of List Catamorphisms: Towards Problem Specific Use of Program Templates in IP. In PEPM. https:\/\/doi.org\/10.1145\/1706356.1706375 10.1145\/1706356.1706375","DOI":"10.1145\/1706356.1706375"},{"key":"e_1_3_2_53_2","doi-asserted-by":"crossref","unstructured":"G. P. Huet. 1975. A Unification Algorithm for Typed \u03bb-Calculus. In Theoretical Computer Science.","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","unstructured":"M. B. James Z. Guo Z. Wang S. Doshi H. Peleg R. Jhala and N. Polikarpova. 2020. Digging for Fold: Synthesis-Aided API Discovery for Haskell. In OOPSLA. https:\/\/doi.org\/10.1145\/3428273 10.1145\/3428273","DOI":"10.1145\/3428273"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"J. Jeon X. Qiu J. S. Foster and A. Solar-Lezama. 2015. JSketch: Sketching for Java. In ESEC\/FSE. https:\/\/doi.org\/10.1145\/2786805.2803189 10.1145\/2786805.2803189","DOI":"10.1145\/2786805.2803189"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","unstructured":"S. Jha S. Gulwani S. A. Seshia and A. Tiwari. 2010. Oracle-Guided Component-Based Program Synthesis. In ICSE. https:\/\/doi.org\/10.1145\/1806799.1806833 10.1145\/1806799.1806833","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","unstructured":"N. D. Jones P. Sestoft and H. S\u00f8ndergaard. 1989. Mix: A Self-Applicable Partial Evaluator for Experiments in Compiler Generation. In LISP and Symbolic Computation. https:\/\/doi.org\/10.1007\/BF01806312 10.1007\/BF01806312","DOI":"10.1007\/BF01806312"},{"key":"e_1_3_2_58_2","unstructured":"S. P. Jones and S. Graf. 2023. Triemaps that match. arXiv:2302.08775 [cs.PL]"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"S. Kamil A. Cheung S. Itzhaky and A. Solar-Lezama. 2016. Verified Lifting of Stencil Computations. In PLDI. https:\/\/doi.org\/10.1145\/2908080.2908117 10.1145\/2908080.2908117","DOI":"10.1145\/2908080.2908117"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","unstructured":"T. Knoth D. Wang N. Polikarpova and J. Hoffmann. 2019. Resource-Guided Program Synthesis. In PLDI. https:\/\/doi.org\/10.1145\/3314221.3314602 10.1145\/3314221.3314602","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_3_2_61_2","unstructured":"D. Kocetkov R. Li L. B. Allal J. Li C. Mou C. M. Ferrandis Y. Jernite M. Mitchell S. Hughes T. Wolf D. Bahdanau L. von Werra and H. de Vries. 2022. The Stack: 3 TB of permissively licensed source code. arXiv:2211.15533 [cs.CL]"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"J. Koppel Z. Guo E. de Vries A. Solar-Lezama and N. Polikarpova. 2022. Searching Entangled Program Spaces. In ICFP. https:\/\/doi.org\/10.1145\/3547622 10.1145\/3547622","DOI":"10.1145\/3547622"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","unstructured":"D. Kozen. 1997. Kleene Algebra with Tests. In TOPLAS. https:\/\/doi.org\/10.1145\/256167.256195 10.1145\/256167.256195","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","unstructured":"S. Krishnamoorthy M. Baskaran U. Bondhugula J. Ramanujam A. Rountev and P. Sadayappan. 2007. Effective Automatic Parallelization of Stencil Computations. In PLDI. https:\/\/doi.org\/10.1145\/1250734.1250761 10.1145\/1250734.1250761","DOI":"10.1145\/1250734.1250761"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","unstructured":"S. Laddad C. Power M. Milano A. Cheung and J. M. Hellerstein. 2022. Katara: Synthesizing CRDTs with Verified Lifting. In OOPSLA. https:\/\/doi.org\/10.1145\/3563336 10.1145\/3563336","DOI":"10.1145\/3563336"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","unstructured":"M. Lange E. Lozes and M. Vargas Guzm\u00e1n. 2014. Model-Checking Process Equivalences. In Theoretical Computer Science. https:\/\/doi.org\/10.1016\/j.tcs.2014.08.020 10.1016\/j.tcs.2014.08.020","DOI":"10.1016\/j.tcs.2014.08.020"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","unstructured":"W. Lee and H. Cho. 2023. Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions. In POPL. https:\/\/doi.org\/10.1145\/3571263 10.1145\/3571263","DOI":"10.1145\/3571263"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","unstructured":"W. Lee K. Heo R. Alur and M. Naik. 2018. Accelerating Search-Based Program Synthesis Using Learned Probabilistic Models. In PLDI. https:\/\/doi.org\/10.1145\/3192366.3192410 10.1145\/3192366.3192410","DOI":"10.1145\/3192366.3192410"},{"key":"e_1_3_2_69_2","unstructured":"Tomer Libal and A. Steen. 2016. Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers. In PAAR. https:\/\/hal.science\/hal-01424749"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","unstructured":"N. P. Lopes and J. Monteiro. 2016. Automatic Equivalence Checking of Programs with Uninterpreted Functions and Integer Arithmetic. In STTT. https:\/\/doi.org\/10.1007\/s10009-015-0366-1 10.1007\/s10009-015-0366-1","DOI":"10.1007\/s10009-015-0366-1"},{"key":"e_1_3_2_71_2","doi-asserted-by":"crossref","unstructured":"J. Lubin and S. E. Chasins. 2021. How Statically-Typed Functional Programmers Write Code. In OOPSLA. https:\/\/doi.org\/10.1145\/3485532","DOI":"10.1145\/3485532"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","unstructured":"J. Lubin N. Collins C. Omar and R. Chugh. 2020. Program Sketching with Live Bidirectional Evaluation. In ICFP. https:\/\/doi.org\/10.1145\/3408991 10.1145\/3408991","DOI":"10.1145\/3408991"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","unstructured":"J. Lubin J. Ferguson K. Ye J. Yim and S. E. Chasins. 2024. Cobbler Virtual Machine. https:\/\/doi.org\/10.5281\/zenodo.10802503 10.5281\/zenodo.10802503","DOI":"10.5281\/zenodo.10802503"},{"key":"e_1_3_2_74_2","doi-asserted-by":"crossref","unstructured":"D. Mandelin L. Xu R. Bod\u00edk and D. Kimelman. 2005. Jungloid Mining: Helping to Navigate the API Jungle. In PLDI.","DOI":"10.1145\/1065010.1065018"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","unstructured":"B. Mariano Y. Chen Y. Feng G. Durrett and I. Dillig. 2022. Automated Transpilation of Imperative to Functional Code Using Neural-Guided Program Synthesis. In OOPSLA. https:\/\/doi.org\/10.1145\/3527315 10.1145\/3527315","DOI":"10.1145\/3527315"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","unstructured":"B. Mariano J. Reese S. Xu T. Nguyen X. Qiu J. S. Foster and A. Solar-Lezama. 2019. Program Synthesis with Algebraic Library Specifications. In OOPSLA. https:\/\/doi.org\/10.1145\/3360558 10.1145\/3360558","DOI":"10.1145\/3360558"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","unstructured":"E. Meijer M. Fokkinga and R. Paterson. 1991. Functional Programming with Bananas Lenses Envelopes and Barbed Wire. In FPCA. https:\/\/doi.org\/10.1007\/3540543961_7 10.1007\/3540543961_7","DOI":"10.1007\/3540543961_7"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","unstructured":"N. Meng M. Kim and K. S. McKinley. 2013. Lase: Locating and Applying Systematic Edits by Learning from Examples. In ICSE. https:\/\/doi.org\/10.1109\/ICSE.2013.6606596 10.1109\/ICSE.2013.6606596","DOI":"10.1109\/ICSE.2013.6606596"},{"key":"e_1_3_2_79_2","unstructured":"A. K. Menon O. Tamuz S. Gulwani B. Lampson and A. T. Kalai. 2013. A Machine Learning Framework for Programming by Example. In ICML."},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","unstructured":"A. Miltner A. T. Nu\u00f1ez A. Brendel S. Chaudhuri and I. Dillig. 2022. Bottom-up Synthesis of Recursive Functional Programs Using Angelic Execution. In POPL. https:\/\/doi.org\/10.1145\/3498682 10.1145\/3498682","DOI":"10.1145\/3498682"},{"key":"e_1_3_2_81_2","unstructured":"N. Mitchell. [n. d.]. hlint: Source code suggestions. https:\/\/hackage.haskell.org\/package\/hlint. Accessed: 2024-03-19."},{"key":"e_1_3_2_82_2","doi-asserted-by":"crossref","unstructured":"D. Mordvinov and G. Fedyukovich. 2017. Synchronizing Constrained Horn Clauses. In LPAR.","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"e_1_3_2_83_2","doi-asserted-by":"crossref","unstructured":"N. Mulleners J. Jeuring and B. Heeren. 2023. Program Synthesis Using Example Propagation. In PADL.","DOI":"10.1007\/978-3-031-24841-2_2"},{"key":"e_1_3_2_84_2","doi-asserted-by":"crossref","unstructured":"D. Nam B. Ray S. Kim X. Qu and S. Chandra. 2022. Predictive Synthesis of API-centric Code. In MAPS.","DOI":"10.1145\/3520312.3534866"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","unstructured":"C. Nandi M. Willsey A. Anderson J. R. Wilcox E. Darulova D. Grossman and Z. Tatlock. 2020. Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations. In PLDI. https:\/\/doi.org\/10.1145\/3385412.3386012 10.1145\/3385412.3386012","DOI":"10.1145\/3385412.3386012"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","unstructured":"C. Nandi M. Willsey A. Zhu Y. R. Wang B. Saiki A. Anderson A. Schulz D. Grossman and Z. Tatlock. 2021. Rewrite Rule Inference Using Equality Saturation. In OOPSLA. https:\/\/doi.org\/10.1145\/3485496 10.1145\/3485496","DOI":"10.1145\/3485496"},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","unstructured":"T. Nipkow. 1993. Functional Unification of Higher-Order Patterns. In LICS. https:\/\/doi.org\/10.1109\/LICS.1993.287599 10.1109\/LICS.1993.287599","DOI":"10.1109\/LICS.1993.287599"},{"key":"e_1_3_2_88_2","volume-title":"Ph. D. Dissertation","author":"Norell U.","year":"2007","unstructured":"U. Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. Ph. D. Dissertation. Chalmers University of Technology."},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","unstructured":"P.-M. Osera and S. Zdancewic. 2015. Type-and-Example-Directed Program Synthesis. In PLDI. https:\/\/doi.org\/10.1145\/2737924.2738007 10.1145\/2737924.2738007","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_3_2_90_2","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. 1986. Natural Deduction as Higher-Order Resolution. In Journal of Logic Programming.","DOI":"10.1016\/0743-1066(86)90015-4"},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","unstructured":"P. M. Phothilimthana T. Jelvis R. Shah N. Totla S. Chasins and R. Bodik. 2014. Chlorophyll: Synthesis-Aided Compiler for Low-Power Spatial Architectures. In PLDI. https:\/\/doi.org\/10.1145\/2594291.2594339 10.1145\/2594291.2594339","DOI":"10.1145\/2594291.2594339"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","unstructured":"P. M. Phothilimthana A. Thakur R. Bodik and D. Dhurjati. 2016. GreenThumb: Superoptimizer Construction Framework. In CC. https:\/\/doi.org\/10.1145\/2892208.2892233 10.1145\/2892208.2892233","DOI":"10.1145\/2892208.2892233"},{"key":"e_1_3_2_93_2","doi-asserted-by":"crossref","unstructured":"P. M. Phothilimthana A. Thakur R. Bodik and D. Dhurjati. 2016. Scaling up Superoptimization. In ASPLOS.","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_2_94_2","doi-asserted-by":"crossref","unstructured":"B. Pientka. 2009. Higher-Order Term Indexing Using Substitution Trees. In TOCL.","DOI":"10.1145\/1614431.1614437"},{"key":"e_1_3_2_95_2","doi-asserted-by":"publisher","unstructured":"N. Polikarpova I. Kuraj and A. Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. In PLDI. https:\/\/doi.org\/10.1145\/2908080.2908093 10.1145\/2908080.2908093","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_96_2","doi-asserted-by":"publisher","unstructured":"M. Raza S. Gulwani and N. Milic-Frayling. 2014. Programming by Example Using Least General Generalizations. In AAAI Conference on Artificial Intelligence. https:\/\/doi.org\/10.1609\/aaai.v28i1.8744 10.1609\/aaai.v28i1.8744","DOI":"10.1609\/aaai.v28i1.8744"},{"key":"e_1_3_2_97_2","doi-asserted-by":"publisher","unstructured":"R. Rolim G. Soares L. D\u2019Antoni O. Polozov S. Gulwani R. Gheyi R. Suzuki and B. Hartmann. 2017. Learning Syntactic Program Transformations from Examples. In ICSE. https:\/\/doi.org\/10.1109\/ICSE.2017.44 10.1109\/ICSE.2017.44","DOI":"10.1109\/ICSE.2017.44"},{"key":"e_1_3_2_98_2","doi-asserted-by":"crossref","unstructured":"R. Rugina and M. Rinard. 1999. Automatic Parallelization of Divide and Conquer Algorithms. In PPoPP.","DOI":"10.1145\/301104.301111"},{"key":"e_1_3_2_99_2","doi-asserted-by":"crossref","unstructured":"E. Schkufza R. Sharma and A. Aiken. 2013. Stochastic Superoptimization. In ASPLOS.","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_3_2_100_2","doi-asserted-by":"crossref","unstructured":"R. Sharma E. Schkufza B. Churchill and A. Aiken. 2013. Data-Driven Equivalence Checking. In OOPSLA.","DOI":"10.1145\/2509136.2509509"},{"key":"e_1_3_2_101_2","doi-asserted-by":"publisher","unstructured":"K. C. Shashidhar M. Bruynooghe F. Catthoor and G. Janssens. 2005. Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code. In DATE. https:\/\/doi.org\/10.1109\/DATE.2005.163 10.1109\/DATE.2005.163","DOI":"10.1109\/DATE.2005.163"},{"key":"e_1_3_2_102_2","doi-asserted-by":"crossref","unstructured":"K. Shi D. Bieber and R. Singh. 2022. TF-Coder: Program Synthesis for Tensor Manipulations. In TOPLAS.","DOI":"10.1145\/3517034"},{"key":"e_1_3_2_103_2","doi-asserted-by":"publisher","unstructured":"C. Smith and A. Albarghouthi. 2016. MapReduce Program Synthesis. In PLDI. https:\/\/doi.org\/10.1145\/2908080.2908102 10.1145\/2908080.2908102","DOI":"10.1145\/2908080.2908102"},{"key":"e_1_3_2_104_2","doi-asserted-by":"publisher","unstructured":"C. Smith and A. Albarghouthi. 2019. Program Synthesis with Equivalence Reduction. In VMCAI. https:\/\/doi.org\/10.1007\/978-3-030-11245-5_2 10.1007\/978-3-030-11245-5_2","DOI":"10.1007\/978-3-030-11245-5_2"},{"key":"e_1_3_2_105_2","doi-asserted-by":"publisher","unstructured":"A. Solar-Lezama L. Tancau R. Bodik S. Seshia and V. Saraswat. 2006. Combinatorial Sketching for Finite Programs. In ASPLOS. https:\/\/doi.org\/10.1145\/1168857.1168907 10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_106_2","doi-asserted-by":"publisher","unstructured":"M. Sousa and I. Dillig. 2016. Cartesian Hoare Logic for Verifying K-Safety Properties. In PLDI. https:\/\/doi.org\/10.1145\/2908080.2908092 10.1145\/2908080.2908092","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_2_107_2","doi-asserted-by":"crossref","unstructured":"J. Swan K. Krawiec and Z. A. Kocsis. 2019. Stochastic Synthesis of Recursive Functions Made Easy with Bananas Lenses Envelopes and Barbed Wire. In Genetic Programming and Evolvable Machines.","DOI":"10.1007\/s10710-019-09347-3"},{"key":"e_1_3_2_108_2","doi-asserted-by":"publisher","unstructured":"R. Tate M. Stepp Z. Tatlock and S. Lerner. 2009. Equality Saturation: A New Approach to Optimization. In POPL. https:\/\/doi.org\/10.1145\/1480881.1480915 10.1145\/1480881.1480915","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_109_2","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.7313584 10.5281\/zenodo.7313584","DOI":"10.5281\/zenodo.7313584"},{"key":"e_1_3_2_110_2","doi-asserted-by":"publisher","unstructured":"The Pandas Development Team. 2020. Pandas. https:\/\/doi.org\/10.5281\/zenodo.3509134 10.5281\/zenodo.3509134","DOI":"10.5281\/zenodo.3509134"},{"key":"e_1_3_2_111_2","unstructured":"F. Theiss and C. Benzm\u00fcller. 2006. Term Indexing for the LEO-II Prover. In IWIL."},{"key":"e_1_3_2_112_2","unstructured":"E. Torlak and D. Jackson. 2007. Kodkod: A Relational Model Finder. In TACAS."},{"key":"e_1_3_2_113_2","doi-asserted-by":"crossref","unstructured":"H. Unno T. Terauchi and E. Koskinen. 2021. Constraint-Based Relational Verification. In CAV.","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_2_114_2","doi-asserted-by":"publisher","unstructured":"S. Verdoolaege G. Janssens and M. Bruynooghe. 2009. Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences. In CAV. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_44 10.1007\/978-3-642-02658-4_44","DOI":"10.1007\/978-3-642-02658-4_44"},{"key":"e_1_3_2_115_2","unstructured":"Verse Lab. [n. d.]. Ego. https:\/\/verse-lab.github.io\/ego\/ego\/index.html. Accessed: 2023-11-14."},{"key":"e_1_3_2_116_2","doi-asserted-by":"publisher","unstructured":"P. Wadler. 1988. Deforestation: Transforming Programs to Eliminate Trees. In Theoretical Computer Science. https:\/\/doi.org\/10.1016\/0304-3975(90)90147-A 10.1016\/0304-3975(90)90147-A","DOI":"10.1016\/0304-3975(90)90147-A"},{"key":"e_1_3_2_117_2","doi-asserted-by":"crossref","unstructured":"Y. R. Wang S. Hutchison J. Leang B. Howe and D. Suciu. 2020. SPORES: Sum-Product Optimization via Relational Equality Saturation for Large Scale Linear Algebra. In Proceedings of the VLDB Endowment.","DOI":"10.14778\/3407790.3407799"},{"key":"e_1_3_2_118_2","doi-asserted-by":"publisher","unstructured":"M. Willsey C. Nandi Y. R. Wang O. Flatt Z. Tatlock and P. Panchekha. 2021. egg: Fast and Extensible Equality Saturation. In POPL. https:\/\/doi.org\/10.1145\/3434304 10.1145\/3434304","DOI":"10.1145\/3434304"},{"key":"e_1_3_2_119_2","doi-asserted-by":"publisher","unstructured":"H. Yang. 2007. Relational Separation Logic. In Theoretical Computer Science. https:\/\/doi.org\/10.1016\/j.tcs.2006.12.036 10.1016\/j.tcs.2006.12.036","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_2_120_2","unstructured":"Y. Yang P. M. Phothilimtha Y. R. Wang M. Willsey S. Roy and J. Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. In MLSys."},{"key":"e_1_3_2_121_2","doi-asserted-by":"publisher","unstructured":"Y. Yuan A. Radhakrishna and R. Samanta. 2023. Trace-Guided Inductive Synthesis of Recursive Functional Programs. In PLDI. https:\/\/doi.org\/10.1145\/3591255 10.1145\/3591255","DOI":"10.1145\/3591255"},{"key":"e_1_3_2_122_2","unstructured":"M. Zalewski. [n. d.]. American Fuzzy Lop. https:\/\/lcamtuf.coredump.cx\/afl\/. Accessed: 2023-07-06."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656453","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656453","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:43:08Z","timestamp":1751661788000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656453"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":121,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656453"],"URL":"https:\/\/doi.org\/10.1145\/3656453","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}