InteractionTrees
Program representation library
A library for representing recursive and impure programs in the Coq proof assistant language.
A Library for Representing Recursive and Impure Programs in Coq
206 stars
16 watching
51 forks
Language: Coq
last commit: about 1 year ago
Linked from 2 awesome lists
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 168 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
| 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 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
| ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
| coq-community/dblib | A Coq library for manipulating binding structures in syntax with binders. | 30 |
 uds-psl/coq-library-undecidability | A collection of mechanized undecidability proofs in Coq | 111 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 191 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 inqwire/sqir | An intermediate representation for quantum programs used in verified optimization of quantum circuits | 80 |