linear-logic
Linear logic encoder
An encoding of linear logic in Coq with minimal examples and automated proofs
An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
21 stars
5 watching
3 forks
Language: Coq
last commit: over 4 years agoRelated projects:
| Repository | Description | Stars |
|---|---|---|
 ekmett/linear-logic | An implementation of intuitionistic linear logic using Haskell. | 83 |
 quix/linalg | A Ruby library for efficient linear algebra computations and matrix operations. | 108 |
 plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 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 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
 inqwire/qwire | A language and formal verification tool for quantum circuits | 95 |
| coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 formal-land/coq-of-ocaml | Transforms OCaml code into formal, verifiable Coq code to prove complex properties | 255 |
 ornl-qci/qcor | A compiler and language extension for heterogeneous quantum-classical computing | 11 |
| ekmett/linear | A set of low-dimensional linear algebra primitives for use in Haskell programs | 203 |
| coq-community/alea | A library for reasoning about randomized algorithms in Coq | 25 |