EGRAPHS 2026
as the organisers put it
Research in the EGRAPHS Community has recently exploded in both quantity and diversity. The data structure that powers SMT solvers is now seeing use in synthesis, optimization, and verification via equality saturation and related techniques. In addition to recent advances in the core data structure and techniques, researchers and practitioners are applying e-graphs to domains such as compilers, floating point accuracy, test generation, computational fabrication, automatic vectorization, deep learning compute graphs, symbolic computation, and more. The fifth EGRAPHS workshop will bring toge ...
who it's for
compiler engineers, programming language researchers, formal methods researchers, optimization engineers, verification engineers, tool developers, high performance computing engineers
topics
equality saturation techniques; memory-scalable equality saturation; e-graphs modulo theories; associative-commutative canonization; AC multiset matching; ILP-based extraction from e-graphs; answer set programming extraction; Knuth-Bendix completion for rewrites; profile-guided numerical rewriting; recursive fixed-point extraction with e-graphs; stochastic search versus equality saturation; top-down library learning for e-graphs
| title | author | length |
|---|---|---|
| A Joint Approach to Instruction Scheduling and Algebraic Rewriting with E-Graphs | Qiantan Hong, Rupanshu Soi, Alex Aiken | 19m |
Scheduling Modulo Equality (SME) builds an e-graph via equality saturation and then encodes extraction as an ILP with binary variables XNT and YCT, latency… | ||
| CERES: Making Equality Saturation Memory-Scalable | Akash Pardeshi, Devansh Jain, Saatvik Lochan, Mihir Tandon, Marco Frigo, Chamika Sudusinghe, Damitha Lenadora, Charith Mendis | 28m |
CERES is a rewrite scheduler that picks a small subset of equality saturation rewrites with a cross-entropy sampler and applies them to keep e-graphs under a… | ||
| A Semi-Persistent E-Graph with Native AC Canonization and Leapfrog AC Matching. | Remi Delmas | 25m |
Describes an equality saturation engine built on a single vector primitive with O(1) snapshots and O(k) restore enabling backtracking inside search, native… | ||
| Lifting E-Graphs: A Function Isn’t a Constant | Philip Zucker | 25m |
Proposes encoding α-equivalence by baking thinning bit vectors into e-nodes so terms carry their context; implements fat identifiers (ID plus thinning) and a… | ||
| Predicate E-Graphs with Symbolic Conditional Rewriting | Anders Ågren Thuné, Johannes Borgström, Lars-Henrik Eriksson, John Högberg, Tjark Weber, Tobias Wrigstad | 14m |
Defines predicate e-graphs that attach Boolean fact-sets to colors and maintain a dynamic pre-order that approximates implication; supports adding edges and… | ||
| Augmenting Rewrite Rule Sets via Knuth-Bendix Completion | Michael Schifferer, Marcel Ullrich, Sebastian Hack | 27m |
Pipeline runs Knuth-Bendix completion (via a tree equational theorem prover) to generate extra oriented rewrite rules, stops after N ≈ 100-rule sweet spot… | ||
| Answer Set Programming for Egg Extraction and More | Ziyi Yang, Ilya Sergey | 24m |
Answer set programming encodes e-graphs as facts and finds low-cost extractions; a naive ASP encoding running with clingo and a core-guided (answer-core)… | ||
| E-graphs modulo theories | Sofia Brookie | 23m |
Develops E-graphs modulo theories to avoid the exponential (≈2^n) blow-up that AC causes, connects AC closure to the word problem and Buchberger‑style… | ||
| Poseidon: Profile-Guided Numerical Rewriting at Full-Application Scale | Siyuan Brant Qian, Vimarsh Sathia, Ivan Ivanov, Jan Hueckelheim, Paul Hovland, William S. Moses | 23m |
Poseidon automatically extracts symbolic expressions from pre-optimized IR, uses a small surrogate profile to get per-instruction sensitivities, and composes… | ||
| Rewrite System Showdown: Stochastic Search vs. EqSat | Qiantan Hong, Rupanshu Soi, Yihong Zhang, Alex Aiken | 23m |
Compares stochastic search (128-thread implementation) to equality saturation (egg/egglog style) across five benchmarks: matrix-chain (optimal known… | ||
| From Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs | Samuel Coward, Cheng Zhang, Philip Zucker, Alexandra Silva | 22m |
Extends e-graphs to represent recursive variables by adding secondary definitional edges that link a variable to its definition without merging, builds a… | ||
| Associativity and Commutativity in Equality Saturation | Tarik Rosin, Marcel Ullrich, Sebastian Hack | 18m |
Extends relational e-matching to handle associative‑commutative operators by storing AC arguments as multisets and adapting tries with a try‑cursor that… | ||
| Optimizing Optimizations, Declaratively: Optimizing the Higher-Order Functions in(…) | Hiromi Ishii | 21m |
Two concrete uses of egglog inside JijModeling 2: resugaring comprehensions reconstructs Python comprehension syntax from map/flat_map/filter and then applies… | ||
| E-Stitch: Top-Down Library Learning for E-Graphs | Kavi Gupta, Maddy Bowers, Armando Solar-Lezama | 23m |
Extends Stitch’s top‑down search to operate over e‑graphs, so rewrites like commutativity are matched rather than missed, and introduces a better lower bound… | ||
| nothing matches | ||