coquedille
Compiler
Translates Coq terms into Cedille terms for a specific domain-specific language
A Coq to Cedille compiler written in Coq
33 stars
6 watching
2 forks
Language: Coq
last commit: about 6 years agoRelated projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
 ptival/peacoq | A Coq-based IDE with OCaml plugin and TypeScript support | 106 |
 mit-plv/rupicola | A toolkit for compiling functional programs into imperative code for performance-critical applications | 51 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
 qt/qttools | Tools and utilities for building and maintaining C++ Qt applications. | 200 |
 cpitclaudel/alectryon | A tool for processing Coq and Lean 4 code embedded in text documents | 237 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
| coq-community/parseque | A Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq. | 42 |
 samuelgruetter/dot-calculus | A formalization of Dependent Object Types (DOT) calculus in Coq to support type safety proofs for a new foundation for Scala's type system | 62 |
 formal-land/coq-of-ocaml | Transforms OCaml code into formal, verifiable Coq code to prove complex properties | 255 |