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 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.



Talia Ringer is the point of contact: tringer@cs.washington.edu.