Jacques: 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..."

2025-11-19T16:47:03Z

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..."

New page

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.

WG211/M25Steuwer - Revision history