C.C. Lemma: induction and lemma discovery in e-graphs
2025-02-20
Cole will present his ICFP 2024 work, C.C. Lemma: induction and lemma discovery in e-graphs.
Abstract
I will discuss how we use e-graphs for the automation of inductive proofs on algebraic data types in our tool C.C. Lemma. E-graphs are a key part of our proof search: we discuss in our paper how their proper use allows us to not only avoid backtracking, but also hypothesize lemmas (in a manner similar to how Ruler hypothesizes rewrite rules). Though I intend for this talk to be accessible to a somewhat broad audience, I hope to delve into some of the specifics of how we use e-graphs and — if time permits — places where we see room for improvement in our use. Some topics I hope to touch on are: rewrites which do the unthinkable and remove nodes from the e-graph, the various intricacies involved with case-splitting an e-graph, and lemma discovery.
Bio
Cole Kurashige is a third-year PhD student at the University of California, San Diego advised by Nadia Polikarpova and Ranjit Jhala. His present research involves verification automation like C.C. Lemma, although he is more broadly interested in research that makes it easier for people to produce reliable code, whether that research is in synthesis, verification, or another area.