coq-elpi
Coq extension library
A Coq plugin embedding Elpi to extend Coq's capabilities with a dialect of lambda-prolog for metaprogramming and scripting.
Coq plugin embedding elpi
139 stars
9 watching
51 forks
Language: Coq
last commit: 9 days ago
Linked from 2 awesome lists
coqextension-languagelambda-prologmetaprogrammingscripting
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 354 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 44 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
 coq/vscoq | A Visual Studio Code extension for Coq proof assistant support | 343 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 ptival/peacoq | A Coq-based IDE with OCaml plugin and TypeScript support | 106 |
| plclub/hs-to-coq | A tool that translates Haskell code to equivalent Coq code | 79 |
 lysxia/coq-simple-io | Provides tools to implement IO programs directly in Coq | 31 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
 eugeneloy/coq_jupyter | A Jupyter notebook kernel for interactive theorem proving with Coq | 94 |