coq-library-undecidability
Undecidability library
A collection of mechanized undecidability proofs in Coq
A library of mechanised undecidability proofs in the Coq proof assistant.
111 stars
7 watching
30 forks
Language: Coq
last commit: about 2 months ago
Linked from 2 awesome lists
coq
coq-community/awesome-coq
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| uds-psl/autosubst2 | A tool for generating Coq code from syntactic theories with variable binders | 17 |
 dmxlarchey/coq-kruskal | A comprehensive library of constructive Coq proofs for Kruskal's tree theorem and related concepts. | 0 |
| 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 |
 deepspec/interactiontrees | A library for representing recursive and impure programs in the Coq proof assistant language. | 203 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 167 |
 uwplse/cheerios | A formally verified serialization library for Coq | 23 |
 unimath/unimath | Formalizes mathematics using the univalent point of view | 961 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
| uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 unicoq/unicoq | An enhanced unification algorithm for Coq | 49 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
| ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 jtassarotti/coq-proba | A Coq-based probability theory library providing results and definitions for discrete probability, measure theory, and probabilistic choice monads. | 49 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 515 |