Rule Inference for Equality Saturation

Equality saturation is an increasingly popular technique in optimizing compilers, synthesizers, and verifiers. However, equality saturation is only as powerful as the rules that it uses, and developing high-quality rulesets is difficult and error-prone.

Our goal is to develop techniques and tools for synthesizing rewrite rules for use in equality saturation applications.

Our code is publicly available on Github, and we encourage people to try using our tools for rule inference. Please reach out to us if you have questions about how to implement your domain in Enumo or Ruler!


October 2023 Ryan presented a poster at OOPSLA 2023.
October 2023 Anjali presented our work on Enumo for her Qualifying Exam
September 2023 Thia presented a poster on derivability in the Student Research Competition at ICFP and won first place in the undergraduate category!
August 2023 Our paper, "Equality Saturation Theory Exploration à la Carte", is accepted at OOPSLA 2023!
October 2021 "Rewrite Rule Inference Using Equality Saturation" receives a Distinguished Paper Award!


OOPSLA 2023 Anjali Pal, Brett Saiki, Cynthia Richey, Ryan Tjoa, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi.
slides talk code
OOPSLA 2021 Chandrakana Nandi, Max Willsey, Amy Zhu, Brett Saiki, Remy Wang, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock.
Distinguished Paper Award
slides talk code


The best way to contact me is by email. Please don't hesitate to reach out with any questions, comments, or ideas!