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.
The plugin for patch-based proof repair (originally named "PUMPKIN PATCH") is available at uwplse/PUMPKIN-PATCH on GitHub.
The plugin for ornament-based proof reuse (individually named "DEVOID") is available at uwplse/ornamental-search on GitHub.
Our support library for Coq plugins, used by both the above plugins, is available at uwplse/coq-plugin-lib on GitHub.
- REPLica: REPL instrumentation for Coq analysis at CPP '20
- 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)
Talia Ringer is the point of contact: email@example.com.