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
396 stars
17 watching
83 forks
Language: Coq
last commit: about 1 month 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. | 45 |
| 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 | 42 |
 lpcic/coq-elpi | Provides an extension language for Coq to manipulate terms containing binders and supports scripting and metaprogramming | 141 |
| 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 | 507 |
| 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 in Coq using optimization and theorem-proving techniques. | 22 |
| coq-community/alea | A library for reasoning about randomized algorithms in Coq | 25 |