EGRAPHS 2024
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 third EGRAPHS workshop will bring toge ...
who it's for
e-graph researchers, compiler engineers, formal methods researchers, verification engineers, hardware designers, programming language researchers, tool developers
topics
disequalities in e-graphs; slotted e-classes (parameterized e-classes); contextual equality saturation; Lean and e-graph proof automation; egglog relational encodings; e-graphs for LLVM IR translation; SpEQ sparse-code translation to libraries; loop saturation for high-level synthesis; e-graph-based RTL power optimization; e-graphs for test-suite reduction; performant dynamically typed e-graphs in Julia
| title | author | length |
|---|---|---|
| Disequalities in E-Graphs: An Experiment | George Zakhour, Pascal Weisenburger, Guido Salvaneschi | 25m |
Implements disequalities inside egg as a lightweight extension called dis that adds a forbid field to e-classes and a disunion operation to record class-level… | ||
| Bridging Syntax and Semantics of Lean Expressions in E-Graphs | Marcus Rossel, Andrés Goens | 28m |
Prototype proof automation encodes Lean expressions into egg and uses equality saturation (egg backend) to synthesize explanations that Lean then checks… | ||
| superVer: Verifying Probabilistic Independence of Systems of Expressions using(…) | Alexander Treff, Pajam Pauls, Maximilian Orlt, Marc Gourjon | 23m |
superVer implements a Rust tool built on the egg equality‑saturation library to decide when sets of algebraic probes have joint distributions independent of… | ||
| Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs | Adrian Lehmann, Ben Caldwell, John Reppy, Robert Rand | 22m |
Encodes a dependently typed DSL for symmetric monoidal categories and the ZX calculus into egglog by computing dependent-type arguments as functions and… | ||
| SpEQ: Translation of Sparse Codes using Equivalences | Avery Laird, Bangtian Liu, Nikolaj Bjørner, Maryam Mehri Dehnavi | 28m |
SpEQ is a tool (PLDI 2024) that detects when code matches small reference C implementations by translating LLVM IR into e-graphs, adding memory-version returns… | ||
| Loop Saturation for Scalable High-Level Synthesis | Camille Bossut, Qirun Zhang, Cong "Callie" Hao | 23m |
Prototype Python tooling uses egg based equality saturation to perform loop saturation via array injection, IR detection, loop rerolling and code extraction on… | ||
| Algorithm-Aware Hardware Optimization using E-Graph Rewriting: how should we marry(…) | Jianyi Cheng, Samuel Coward, Rafael Barbalho, Theo Drane | 22m |
SEER orchestrates e-graph rewriting with LLVM MIR passes and an Act-based Intel Rover hardware optimizer, translating between MIR and a custom crand IR… | ||
| Powered by Less: Low Power Circuit Synthesis | Samuel Coward, Theo Drane, Emiliano Morini, George A. Constantinides | 22m |
An automated RTL-to-RTL framework named Rover uses e-graph rewriting to combine arithmetic rewrites with clock/data gating and transparent-register insertion… | ||
| EGSTRA: E-Graph-Based Strategy for Test Suite Reduction and Abstraction | Sabrina Reis, Matthew Sottile | 25m |
EGSTRA uses e-graphs over JSON ASTs to reduce huge program inputs by applying destructive rewrite rules that delete or replace terms, then standard equivalence… | ||
| Performant Dynamically Typed E-Graphs in Pure Julia | Alessandro Cheli, Niklas Heim | 23m |
Metatheory.jl v3 implements e-graphs and equality saturation entirely in Julia, using a term interface that reads/writes expressions from byte buffers to… | ||
| Towards Relational Contextual Equality Saturation | Tyler Hou, Shadaj Laddad, Joseph M. Hellerstein | 19m |
Claims a method to bring contextual equality saturation into the egglog relational model by treating contexts and equivalence relations as lattices and mapping… | ||
| Slotted E-Graphs | Rudi Schneider, Thomas Koehler, Michel Steuwer | 23m |
Implementation builds a new e-graph variant where e-classes are parameterized e-classes that accept slots for bound names, so renaming or removing binders… | ||
| Equivalence Hypergraphs: E-Graphs for Monoidal Theories | Aleksei Tiurin, Chris Barrett, Dan Ghica | 37m |
Presents a categorical construction that generalises e-graphs to arbitrary monoidal theories by representing string diagrams as combinatorial Equivalence… | ||
| E-graphs and Automated Reasoning: Looking back to look forward | Philip Zucker | 38m |
Argues that e-graphs are essentially an instance of ground completion = e-graph rewriting, demonstrates a Python tool that inverts the completion/tree diagram… | ||
| SpEQ: Translation of Sparse Codes using Equivalences | Avery Laird, Bangtian Liu, Nikolaj Bjørner, Maryam Mehri Dehnavi | 19m |
SpEQ detects sparse-data semantics via equivalence checks that prove a CSR-style loop is equivalent to a dense reference, then uses e-graphs (equality… | ||
| nothing matches | ||