Proof repair across type equivalences

Talia Ringer, Ran Dair Porter, Nathaniel Yazdani, John Leo, Dan Grossman

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationPLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
EditorsStephen N. Freund, Eran Yahav
PublisherAssociation for Computing Machinery
Pages112-127
Number of pages16
ISBN (Electronic)9781450383912
DOIs
StatePublished - Jun 18 2021
Externally publishedYes
Event42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021 - Virtual, Online, Canada
Duration: Jun 20 2021Jun 25 2021

Conference

Conference42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021
Country/TerritoryCanada
CityVirtual, Online
Period6/20/216/25/21

Keywords

  • proof engineering
  • proof repair
  • proof reuse

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Proof repair across type equivalences'. Together they form a unique fingerprint.

Cite this