Zachary Tatlock
University of Washington, WA·Computer Science
Compilers, database query optimizers, and theorem provers share a basic problem: deciding when two programs or expressions are equivalent, so that a slower or less accurate version can be swapped for a better one. Traditional tools apply rewrite rules ("find and replace" rules for code) one at a time.
- Fields
Computer Science
Mathematics & Statistics
- Topics
equality saturation
e-graphs
egg
- Grants
- 4 known grants, through Jul 2030
What they work on
- Speed up and extend the egg equality saturation library with relational e-matching (faster searches for places to apply rules), sketch-based extraction for choosing the best program, and destructive rewriting to control e-graph blow-up.
- Build a unified framework that combines Datalog, a logic-based query language, with equality reasoning in e-graphs, and speed it up with database techniques such as semi-naive evaluation and worst-case optimal joins.
- Determine theoretical conditions that guarantee equality saturation finishes, adapting results from term rewriting, the database chase, and tree automata.
- Develop persistent e-graphs in the egglog engine that are reused across program edits. Use e-graph distillation and a garbage-collection layer to keep only high-value fragments.
- Design an iterative extraction algorithm that enforces global rules such as memory linearity and control-flow dominance through counterexample-guided refinement. Evaluate it in the Herbie and eggcc compilers.
- Extend the FPBench floating-point standard to record inputs, platforms, code locations, and error bounds. Collect real-world numerical benchmarks and build a single interface that coordinates existing numerical analysis tools.
More about the research
In that approach, the order in which rules are applied changes the result, and no single order works best for every program. Equality saturation is a different approach. It applies all rewrite rules at once and stores every equivalent version of a program compactly in a data structure called an e-graph (equality graph). A tool can then pick the best version afterward. The team's framework for this, called egg, has been used to build compilers for machine learning, design tools for 3D printing, and tools that repair rounding errors in scientific code. The lab's grants make equality saturation faster and more scalable, give it stronger theoretical foundations, and make it easier for others to use. A related grant applies these kinds of tools to errors in computer arithmetic.
Why it matters
Faster, reusable e-graphs could make compilation quicker and use less energy in software development, scientific computing, and AI workflows. They could also make advanced code optimization practical for developers who lack large computing budgets. Better equivalence checking could improve compilers, database query optimizers, and theorem provers. Shared numerical tools and benchmarks could help scientists and engineers write floating-point software that is more accurate and reliable across different hardware.
Known grants
From NIH and NSF research grants. Labs often have other funding we can't see.
Collaborative Research: SHF: Scaling E-graphs for Incremental Analysis and Optimization
NSF · Aug 2026 – Jul 2030
Collaborative Research: CIRC: Medium: New: Workbench for Reliable and Efficient Numerics
NSF · Jul 2024 – Jun 2027
CCRI: New: Incubating egg: Developing a Scalable, Cohesive Equality Saturation Ecosystem and Community
NSF · Jun 2023 – May 2027
Closest labs
Jiajia Li
North Carolina State University, NC·Computer Science
Build a multi-level auto-tuning system that selects GPU execution strategies for ragged tensors, whose pieces vary in size, keeping overhead low via efficient sampling and search-space pruning.
Qirun Zhang
Georgia Institute of Technology, GA·Computer Science·Early-career
Characterize what the InterDyck graph abstraction can and cannot express. This is a graph model of programs with matched-edge patterns that represents program meaning for analysis.
Nathaniel Bleier
University of Michigan, MI·Computer Science
Combine learning-guided program synthesis with automated logical reasoning to generate instruction sequences, accelerator control codes and microcoded expansions that are formally proven equivalent to the original program.
The school
University of Washington: 81 labs on PI Pages, $1.7B a year on research, 694 research doctorates a year.
Reach out
A start for your email. Fill in the brackets.