Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Fri 22 Jan 2021 18:40 - 18:50 at POPL-B - Logic and Decision Procedures

An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites.

This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation’s distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation.

We implemented these techniques in a new open-source library called egg. Our case studies on three previously published applications of equality saturation highlight how egg’s performance and flexibility enable state-of-the-art results across diverse domains.

Fri 22 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:00: Logic and Decision ProceduresPOPL at POPL-B
18:30 - 18:40
Cyclic Proofs, System T, and the Power of Contraction
Denis KuperbergLIP, ENS de Lyon, Laureline PinaultLIP, ENS de Lyon, Damien PousCNRS
Link to publication DOI
18:40 - 18:50
egg: Fast and Extensible Equality SaturationDistinguished Paper
Max WillseyUniversity of Washington, USA, Chandrakana NandiUniversity of Washington, USA, Yisu Remy WangUniversity of Washington, Oliver FlattUniversity of Utah, Zachary TatlockUniversity of Washington, Seattle, Pavel PanchekhaUniversity of Utah
Link to publication DOI Pre-print
18:50 - 19:00
Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS
David ZhaoThe University of Sydney, Pavle SuboticMicrosoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard ScholzUniversity of Sydney, Australia
Link to publication DOI