PUMPKIN PATCH
A tool for proof repair
PUMPKIN PATCH (Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker) is a suite of Coq plugins for proof repair, reuse, and evolution. These plugins are the focus of a research project in the PLSE group of UW CSE. This project is associated with a broader effort on research in proof engineering.
To learn more about our plugins, check out the source code and/or our published articles.
Source code
The PUMPKIN PATCH proof repair plugin suite is available at uwplse/PUMPKIN-PATCH on GitHub.
The plugin for proof repair across type equivalences (individually named "PUMPKIN Pi," formerly "DEVOID") is available at uwplse/pumpkin-pi on GitHub.
Our support library for Coq plugins, used by both the above plugins, is available at uwplse/coq-plugin-lib on GitHub.
Publications
- Proof Repair PhD thesis (defense video)
- Proof Repair across Type Equivalences at PLDI '21 (talk video)
- REPLica: REPL instrumentation for Coq analysis at CPP '20 (talk video)
- In collaboration with Alex Sanchez-Stern and Sorin Lerner of UCSD CSE
- Ornaments for Proof Reuse in Coq at ITP '19 (talk video)
- Adapting Proof Automation to Adapt Proofs at CPP '18 (talk video)
Contact
Talia Ringer is the main point of contact: talia@dependenttyp.es.
