Speaker: Max Willsey
Location: Soda 380
Date: September 27, 2023
Time: 11 AM – 12 PM PST
Title: “E-Graphs + Datalog = Declarative Program Analysis & Optimization”
Abstract:
I’ll talk about our recent work on egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, it supports efficient incremental execution, cooperating analyses, and lattice-based reasoning. Like EqSat, it supports term rewriting, efficient congruence closure, and extraction of optimized terms. We have successfully used it to replace (and beat!) both conventional Datalog and equality saturation tools. This work is by no means done, as there are big next steps that I hope will turn this system into a unified “one stop shop” for declarative program analysis & optimization. I’ll talk about some of the challenges that stand between us and the goal, most of which are in the form of a wishlist of extensions or efficient implementations of Datalog features.