Talk: E-Graphs for Next-Gen Programming Language Tools

LIVE STREAM: https://uwmadison.zoom.us/j/94267055929?pwd=KzFGanRsck55RGpxSEtLNWF5Ni85dz09

Abstract: Building a state-of-the-art program optimizer, synthesizer, or verifier is still a gargantuan task for even programming language (PL) experts. Much of this challenge stems from the fact that term rewriting, a ubiquitous approach to manipulating programs, only works with one version of a program at a time. As a result, the system builder must carefully consider every program manipulation, lest they accidentally "take a wrong turn" and miss out on optimization opportunities. For non-PL-experts, these difficulties prevent application of PL techniques to domains that might otherwise greatly benefit from them.

This talk will describe a data structure called the e-graph and a technique called equality saturation that together allow one to store and manipulate many equivalent versions of a program simultaneously. Recent advances like delayed congruence closure and lattice-based "e-class analyses", both embodied in the egg e-graph toolkit, have made this approach fast and flexible enough for academic and industrial use in areas including deep learning, carpentry, 3D design, and floating point arithmetic. This talk will also present recent discoveries that connect equality saturation to relational databases. The result is faster, simpler, and theoretically optimal implementations of equality saturation.

Bio: Max Willsey is a post-doctoral researcher in computer science at the University of Washington working with Zach Tatlock. His research connects programming languages, database theory, and formal methods to make it easier to build state-of-the-art program optimizers, synthesizers, and verifiers. He leads the development of the egg toolkit used by many research groups and companies, leading to several publications and two Distinguished Paper awards. He earned his Ph.D. at the University of Washington advised by Luis Ceze.