miniKanren-coq
Relational programming semantics
A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages
A certified semantics for relational programming workout.
26 stars
3 watching
4 forks
Language: Coq
last commit: almost 6 years agoRelated projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 46 |
| coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
| coq-community/dblib | A Coq library for manipulating binding structures in syntax with binders. | 30 |
 snu-sf/promising-coq | Development of a promising semantics for relaxed-memory concurrency | 33 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 xavierleroy/cdf-sem-meca | This project provides a development environment and software tools for formalizing the semantics of programming languages in the Coq proof assistant. | 21 |
| xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
| 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/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 30 |
 llee454/functional-algebra | A Coq formalization of abstract algebra using functional programming style | 28 |