Equality Saturation: Progress and Open Questions

In equational reasoning, congruence closure is known for being a semi-decision procedure that’s efficient in practice. Equality saturation can be seen as an extension of congruence closure that allows conditional rewriting and optimizing terms in the equivalence classes. It has been very successful in domains beside automated reasoning, like program optimisation in compilers. In this talk we will discuss equality saturation and its advantages. We will also discuss its shortcomings - with either solutions to these shortcomings, or open questions about them.