{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:05:44Z","timestamp":1784199944934,"version":"3.55.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>Equality saturation has gained significant interest as a powerful optimization and reasoning technique. At its heart is the e-graph data structure, that space-efficiently represents equal sub-terms uniquely. An important open problem in this context is extending this efficient representation to languages featuring (bound) variables. Independent of how we represent variables in e-graphs, either as names or nameless (using de Bruijn indices), sharing is broken as sub-terms that differ only in the names of their variables are represented separately. This results in aggressive e-graph growth, bad performance, as well as reduced expressiveness.<\/jats:p>\n                  <jats:p>\n                    In this paper, we present a novel approach to representing bound variables in e-graphs by making them a first-class built-in feature of the data structure. Our\n                    <jats:italic toggle=\"yes\">slotted e-graph<\/jats:italic>\n                    represents terms that differ only by (bound or free) variable names uniquely. To do so, e-classes that represent equivalent terms via e-nodes are parameterized by\n                    <jats:italic toggle=\"yes\">slots<\/jats:italic>\n                    , abstracting over free variables of the represented terms. Referring to an e-class from an e-node now requires relating the variables from its context to the slots of the e-class.\n                  <\/jats:p>\n                  <jats:p>\n                    Our evaluation of\n                    <jats:monospace>slotted<\/jats:monospace>\n                    e-graph uses two case studies from compiler optimization and theorem proving to show that performing equality saturation for languages with bound variables is greatly simplified and that we can solve practically relevant problems that cannot be solved with e-graphs using de Bruijn indices.\n                  <\/jats:p>","DOI":"10.1145\/3729326","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1888-1910","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9151-773X","authenticated-orcid":false,"given":"Rudi","family":"Schneider","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-3567-6890","authenticated-orcid":false,"given":"Marcus","family":"Rossel","sequence":"additional","affiliation":[{"name":"Barkhausen Institut, Dresden, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9062-759X","authenticated-orcid":false,"given":"Amir","family":"Shaikhha","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0409-1363","authenticated-orcid":false,"given":"Andr\u00e9s","family":"Goens","sequence":"additional","affiliation":[{"name":"University of Amsterdam, Amsterdam, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8461-8075","authenticated-orcid":false,"given":"Thomas","family":"K\u0153hler","sequence":"additional","affiliation":[{"name":"CNRS - ICube Lab, Strasbourg, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5048-0741","authenticated-orcid":false,"given":"Michel","family":"Steuwer","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"Gregory Butler. 1984. On computing double coset representatives in permutation groups. In Computational Group Theory: Proceedings of the London Mathematical Society Symposium on Computational Group Theory Michael D. Atkinson (Ed.)."},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571207"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Mario Carneiro. 2024. Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. CoRR abs\/2403.14064 (2024). doi:10.48550\/ARXIV.2403.14064arXiv.2403.14064","DOI":"10.48550\/ARXIV.2403.14064arXiv.2403.14064"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640392"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"Robert Dickerson Prasita Mukherjee and Benjamin Delaware. 2024. KestRel: Relational Verification Using E-Graphs for Program Alignment. CoRR abs\/2404.08106 (2024). doi:10.48550\/ARXIV.2404.08106arXiv:2404.08106","DOI":"10.48550\/ARXIV.2404.08106arXiv:2404.08106"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2006.12.002"},{"key":"e_1_3_2_11_1","doi-asserted-by":"crossref","unstructured":"Dan R Ghica. 2021. Operational semantics with hierarchical abstract syntax graphs. arXiv preprint arXiv:2102.02363 (2021).","DOI":"10.4204\/EPTCS.334.1"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768815030056"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218196704001657"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133901"},{"key":"e_1_3_2_15_1","unstructured":"Thomas Koehler. 2022. A domain-extensible compiler with controllable automation of optimisations. Ph. D. Dissertation."},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803406"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632900"},{"key":"e_1_3_2_18_1","first-page":"19","article-title":"On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic","volume":"53","author":"Lachowski Lukasz","year":"2018","unstructured":"Lukasz Lachowski. 2018. On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic. Reports Math. Log. 53 (2018), 19\u201342. https:\/\/rml.tcs.uj.edu\/r\/ml-53\/02-lachowski.pdf","journal-title":"Reports Math. Log."},{"key":"e_1_3_2_19_1","volume-title":"Algebra","author":"Lang Serge","year":"2012","unstructured":"Serge Lang. 2012. Algebra. Vol. 211. Springer Science & Business Media."},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1142\/3645"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454088"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386012"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_2_25_1","unstructured":"Marcus Rossel. 2024. An Equality Saturation Tactic for Lean. Master's thesis."},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3588717"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Rudi Schneider Marcus Rossel Amir Shaikhha Andr\u00e9s Goens Thomas Koehler and Michel Steuwer. 2025. Slotted E-Graphs Artifact. doi:10.5281\/zenodo.15237515","DOI":"10.5281\/zenodo.15237515"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546549"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO57630.2024.10444787"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527333"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460945.3464953"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2004.06.016"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582016.3582032"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:06:47Z","timestamp":1784196407000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":35,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729326"],"URL":"https:\/\/doi.org\/10.1145\/3729326","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}