@inproceedings{31367fd23a9743c8b9f73525e37e9884,
title = "Proof repair across type equivalences",
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 suggested 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. ",
keywords = "proof engineering, proof repair, proof reuse",
author = "Talia Ringer and Porter, {Ran Dair} and Nathaniel Yazdani and John Leo and Dan Grossman",
note = "Funding Information: This material is based upon work supported by the National Science Foundation Graduate Research Fellowship under Grant No. DGE-1256082. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation. Publisher Copyright: {\textcopyright} 2021 ACM.; 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021 ; Conference date: 20-06-2021 Through 25-06-2021",
year = "2021",
month = jun,
day = "18",
doi = "10.1145/3453483.3454033",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "112--127",
editor = "Freund, {Stephen N.} and Eran Yahav",
booktitle = "PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation",
address = "United States",
}