{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:09:15Z","timestamp":1765667355632,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1521602"],"award-info":[{"award-number":["CCF-1521602"]}],"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":[[2021,8,22]]},"abstract":"<jats:p>An efficient optimizing compiler can perform many cascading rewrites in a single pass, using auxiliary data structures such as variable binding maps, delayed substitutions, and occurrence counts. Such optimizers often perform transformations according to relatively simple rewrite rules, but the subtle interactions between the data structures needed for efficiency make them tricky to write and trickier to prove correct. We present a system for semi-automatically deriving both an efficient program transformation and its correctness proof from a list of rewrite rules and specifications of the auxiliary data structures it requires. Dependent types ensure that the holes left behind by our system (for the user to fill in) are filled in correctly, allowing the user low-level control over the implementation without having to worry about getting it wrong. We implemented our system in Coq (though it could be implemented in other logics as well), and used it to write optimization passes that perform uncurrying, inlining, dead code elimination, and static evaluation of case expressions and record projections. The generated implementations are sometimes faster, and at most 40% slower, than hand-written counterparts on a small set of benchmarks; in some cases, they require significantly less code to write and prove correct.<\/jats:p>","DOI":"10.1145\/3473579","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Deriving efficient program transformations from rewrite rules"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2130-5092","authenticated-orcid":false,"given":"John M.","family":"Li","sequence":"first","affiliation":[{"name":"Princeton University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6009-0325","authenticated-orcid":false,"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"volume-title":"The Third International Workshop on Coq for Programming Languages (CoqPL).","year":"2017","author":"Anand Abhishek","key":"e_1_2_2_1_1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018615"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002839"},{"volume-title":"Standard ML of New Jersey. In 3rd International Symp. on Prog. Lang. Implementation and Logic Programming, Martin Wirsing (Ed.). Springer-Verlag","author":"Andrew","key":"e_1_2_2_4_1"},{"volume-title":"NET. In Symposium on Implementation and Application of Functional Languages. 142\u2013159","year":"2004","author":"Benton Nick","key":"e_1_2_2_5_1"},{"key":"e_1_2_2_6_1","unstructured":"Pierre Chambart Mark Shinwell Leo White and Damien Doligez. 2016. Optimization with Flambda. https:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/flambda.html  Pierre Chambart Mark Shinwell Leo White and Damien Doligez. 2016. Optimization with Flambda. https:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/flambda.html"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80540-7"},{"volume-title":"Functional pearl. J. functional programming, 7, 5","year":"1997","author":"Huet G\u00e9rard","key":"e_1_2_2_9_1"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291220.1291179"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41632"},{"volume-title":"Symp. on Compiler Construction), 21","year":"1986","author":"Kranz D.","key":"e_1_2_2_12_1"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45306-7_5"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.03.022"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040335"},{"key":"e_1_2_2_17_1","unstructured":"Xavier Leroy. 2012. The CompCert verified compiler.  Xavier Leroy. 2012. The CompCert verified compiler."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190215.1190220"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004331"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.44"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005605"},{"volume-title":"Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming. 49\u201360","author":"B\u00e9langer Olivier Savary","key":"e_1_2_2_24_1"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"e_1_2_2_26_1","first-page":"1","article-title":"The MetaCoq Project","author":"Sozeau Matthieu","year":"2020","journal-title":"Journal of Automated Reasoning"},{"volume-title":"Rabbit: a compiler for Scheme","author":"Steele Guy L.","key":"e_1_2_2_27_1"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364531"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706345"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/143103.143120"},{"volume-title":"Domain-specific program generation","author":"Visser Eelco","key":"e_1_2_2_31_1"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.267960"},{"volume-title":"Finding and understanding bugs in C compilers. ACM SIGPLAN Notices (PLDI\u201911), 46, 6","year":"2011","author":"Yang Xuejun","key":"e_1_2_2_33_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473579","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473579","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473579","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473579"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":32,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473579"],"URL":"https:\/\/doi.org\/10.1145\/3473579","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}