On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep

WG211/M25Steuwer

From WG 2.11
Revision as of 17:47, 19 November 2025 by Jacques (talk | contribs) (Created page with "E-Graphs are a core data structure used in automatic reasoning and program optimization. They space-efficiently represent a set of equivalent terms. However, representing programs with bindings in e-graphs using existing techniques quickly defeats the efficiency purpose in many practical applications, as the e-graph represents alpha-equivalent terms many times. In this talk, I am going to present our work on Slotted E-Graphs that augment E-Graphs with a build-in notion...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

E-Graphs are a core data structure used in automatic reasoning and program optimization. They space-efficiently represent a set of equivalent terms.

However, representing programs with bindings in e-graphs using existing techniques quickly defeats the efficiency purpose in many practical applications, as the e-graph represents alpha-equivalent terms many times.

In this talk, I am going to present our work on Slotted E-Graphs that augment E-Graphs with a build-in notion of binders. By taking inspirations from the nominal approach, we are able to build a data-structure that is capable of space-efficiently representing programs with binders and the guarantee that alpha-equivalent terms are represented uniquely.

This talk presents work that has been published at PLDI 2025.

Retrieved from "http://mw.hh.se/wg211/index.php?title=WG211/M25Steuwer&oldid=2842"