@inproceedings{7c8d65ec9fa844239dcb0071f6aa5d1b,
title = "Adapting proof automation to adapt proofs",
abstract = "We extend proof automation in an interactive theorem prover to analyze changes in specifications and proofs. Our approach leverages the history of changes to specifications and proofs to search for a patch that can be applied to other specifications and proofs that need to change in analogous ways. We identify and implement five core components that are key to searching for a patch. We build a patch finding procedure from these components, which we configure for various classes of changes. We implement this procedure in a Coq plugin as a proof-of-concept and use it on real Coq code to change specifications, port definitions of a type, and update the Coq standard library. We show how our findings help drive a future that moves the burden of dealing with the brittleness of small changes in an interactive theorem prover away from the programmer and into automated tooling.",
keywords = "Proof automation, Proof evolution, Proof repair",
author = "Talia Ringer and John Leo and Nathaniel Yazdani and Dan Grossman",
note = "Publisher Copyright: {\textcopyright} 2018 Copyright held by the owner/author(s). Publication rights licensed to the Association for Computing Machinery.; 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 ; Conference date: 08-01-2018 Through 09-01-2018",
year = "2018",
month = jan,
day = "8",
doi = "10.1145/3167094",
language = "English (US)",
series = "CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018",
publisher = "Association for Computing Machinery",
pages = "115--129",
editor = "Amy Felty and June Andronick",
booktitle = "CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018",
address = "United States",
}