lngen
Coq generator
Tool for generating Coq definitions and proofs for locally nameless representations
Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott
30 stars
10 watching
9 forks
Language: Haskell
last commit: about 1 month ago
Linked from 1 awesome list
Related projects:
| Repository | Description | Stars |
|---|---|---|
| plclub/hs-to-coq | A tool that translates Haskell code to equivalent Coq code | 78 |
| plclub/metalib | A Coq-based metatheory library providing tools and examples for mechanizing programming language definitions and reasoning about them. | 71 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 167 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 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 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 eugeneloy/coq_jupyter | A Jupyter notebook kernel for interactive theorem proving with Coq | 94 |
 cogcomp/cogcomp-nlp | A collection of libraries and tools for Natural Language Processing | 472 |
 engineeringsoftware/roosterize | An automated tool for suggesting lemma names in Coq proof assistant projects based on neural network models | 18 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |