coqrel
Logical relation library
A Coq-based library for establishing logical relations in formal verification and proof assistance
Binary logical relations library for the Coq proof assistant
20 stars
8 watching
1 forks
Language: Coq
last commit: 4 months ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 67 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 vafeiadis/hahn | A collection of lemmas and tactics about lists and binary relations for a proof assistant | 30 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 damien-pous/relation-algebra | A library providing modular and axiom-free decision procedures for relation algebra theories in Coq. | 48 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 168 |
| 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 |
| coq-community/dblib | A Coq library for manipulating binding structures in syntax with binders. | 30 |
 certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 39 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
| coq-community/math-classes | A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq | 162 |