Slotted e-graphs are a datastructure for representing congruence relations over terms with variables and binders.

For a higher level introduction to slotted e-graphs, consider

• the talk
• the pre-print

For an example implementation of a Language with binders in slotted e-graphs, consider the RISE implementation in here.

Slotted E-Graphs

In this repository we've implemented slotted e-graphs.

For a higher level introduction to slotted e-graphs, consider the PLDI (2025) talk or paper,

or alternatively the PLDI (2024) workshop talk or paper.

For an example implementation of a Language with binders in slotted e-graphs, consider the RISE implementation in here.

For documentation, see here.