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.



Talia Ringer is the main point of contact: talia@dependenttyp.es.