3 papers
cs.PL2022
Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey +2
Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification…
math.NA2021
An Interval Arithmetic for Robust Error Estimation
Oliver Flatt, Pavel Panchekha
Interval arithmetic is a simple way to compute a mathematical expression to an arbitrary accuracy, widely used for verifying floating-point computations. Yet this simplicity belies…
cs.PL2020
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang +3
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a mor…