arXiv:2010.00774cs.PL
Proof Repair across Type Equivalences
Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.
Abstract
We describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term transformation with a decompiler from proof terms to tactic scripts. The proof term transformation implements transport across equivalences in a way that removes references to the old version of the changed type and does not rely on axioms beyond those Coq assumes. We have implemented this approach in PUMPKIN Pi, an extension to the PUMPKIN PATCH Coq plugin suite for proof repair. We demonstrate PUMPKIN Pi's flexibility on eight case studies, including supporting a benchmark from a user study, easing development with dependent types, porting functions and proofs between unary and binary numbers, and supporting an industrial proof engineer to interoperate between Coq and other verification tools more easily.
This is my thesis area! If you're interested in proof repair, check out my latest work: https://arxiv.org/abs/2010.00774 More on my website: https://dependenttyp.es/ I hope more people work on this problem. It is a big and promising space. And I'll need students soon :)
tlringerView on HNParent context
These problems are more closely related than you imagine. In particular, when you change a program, there is often necessarily more information you must give the computer in order to make the corresponding change in the proof. That additional burden is creativity, and is in many…
tlringerView on HNParent context