pumpkin-pi
Type relationship finder
Automatically discovers and proves relationships between types in Coq to simplify proof development and code reuse.
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
49 stars
11 watching
9 forks
Language: Coq
last commit: 2 months ago algebraic-ornamentscoqcoq-plugindependent-typesdevoidequivalencesornamentsproof-assistantsproof-refactoringproof-repairproof-reusepumpkin-patchpumpkin-pirefactoringrepairtransport
Related projects:
| Repository | Description | Stars |
|---|---|---|
| uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
| uwplse/cheerios | A formally verified serialization library for Coq | 23 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 thery/coqprime | A proof assistant library for prime number certification using elliptic curves and Pocklington certificates | 37 |
 eugeneloy/coq_jupyter | A Jupyter notebook kernel for interactive theorem proving with Coq | 94 |
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 uds-psl/mpctt | A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory | 80 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |
 deepspec/interactiontrees | A library for representing recursive and impure programs in the Coq proof assistant language. | 203 |
 lukaszcz/coqhammer | A tool for automating proof search and verification in dependent type theory using machine learning and external provers. | 218 |