Proofs of Equality in Deductive Databases
M.S. Thesis, Cornell University, 2024
A proof system for extensions of Datalog with equality, giving methods for debugging and verifying the correctness of query results. Includes an elegant proof system for Egglog (an extension of Datalog with equality saturation), a proof checker mechanized in Rocq, and a case study optimizing NetKAT programs with Egglog.