metacoq
Coq manipulator
A tool for formalizing and manipulating Coq terms, providing a foundation for metaprogramming and certified plugins.
Metaprogramming, verified meta-theory and implementation of Coq in Coq
382 stars
17 watching
82 forks
Language: Coq
last commit: 6 days ago
Linked from 2 awesome lists
coqcoq-formalizationmetaprogramming
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 44 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
| coq-community/aac-tactics | Tactics for rewriting and proving equations with associativity and commutativity properties | 29 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 lpcic/coq-elpi | A Coq plugin embedding Elpi to extend Coq's capabilities with a dialect of lambda-prolog for metaprogramming and scripting. | 139 |
| coq-community/sudoku | A formalisation of Sudoku in Coq to solve the puzzle using a naive Davis-Putnam procedure | 20 |
| coq-community/coq-tricks | A resource for discovering useful techniques and tricks in Coq | 503 |
| coq-community/dblib | A Coq library for manipulating binding structures in syntax with binders. | 30 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
 coq-polyhedra/coq-polyhedra | Formalizes convex polyhedra using theorem-proving in Coq | 22 |
| coq-community/alea | A library for reasoning about randomized algorithms in Coq | 25 |