Thesis

I have to graduate

PUMPKIN PATCH 0.1: Ornamental PUMPKIN

This is the first official versioned release of PUMPKIN PATCH, now featuring ornaments!

PUMPKIN PATCH is no longer just a plugin. It is a plugin suite. It includes DEVOID, the paper for which can be found here. The README has been update with information on the plugins that PUMPKIN PATCH contains.

PUMPKIN PATCH itself is still a prototype. A lot more functionality is coming soon, and existing functionality will be improved upon. In the meantime, though, DEVOID opens up a whole new host of possibilities---and all of the functionality described in the DEVOID paper can be used from within PUMPKIN PATCH.

Enjoy!

Update to Coq 8.8

Update PUMPKIN PATCH to Coq 8.8.

Update to Coq 8.6

Update PUMPKIN PATCH to Coq 8.6.

CPP 2018

Code in a frozen state from the CPP 2018 paper "Adapting Proof Automation to Adapt Proofs."