Today, we will read Proof Repair across Type Equivalences [PDF] [DOI] by Talia Ringer, RanDair Porter, Nate Yazdani, John Leo, and Dan Grossman.
This is my work, so I'm obviously biased. But it's the sort of seminal paper of my thesis work on proof repair, or automatically fixing proofs in response to breaking changes. This is for those cases where you don't manage to design things perfectly to begin with, or when a dependency breaks in an unexpected way.
While proof repair has a while to go before it's a common part of proof development, this was the first time we really showed practical applicability. Shameless plug: I have plenty of ongoing work in this space with my students, so super please let me know if you find any of this particularly interesting and want to work on it!
You can find a reading guide and the discussion questions below. A public copy of the slides for this class can be found here.
Please note that this is due the morning before class, so that we can discuss it in person. And please install the artifact before Thursday's class.