color
Formalism library
A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination.
Coq library on rewriting theory and termination
35 stars
3 watching
21 forks
Language: Coq
last commit: almost 2 years agoLinked from 2 awesome lists
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 lysxia/system-f | A formalization of polymorphic lambda calculus with a proof of parametricity theorem. | 33 |
 discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 142 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 foreverbell/verified | A collection of formalized and provable data structures and algorithms in Coq for educational purposes | 46 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
 llee454/functional-algebra | A Coq formalization of abstract algebra using functional programming style | 28 |
 pi8027/lambda-calculus | A formalization of typed and untyped lambda calculus in Coq and Agda2, aiming to provide a rigorous foundation for understanding the properties of these systems. | 78 |
 coq-community/fourcolor | A formal proof of a fundamental result in graph theory using the Coq proof assistant | 174 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 vrahli/nuprlincoq | Formalizes Nuprl's Constructive Type Theory in Coq, focusing on its computation system, type system, inference rules, and consistency. | 44 |
 reynir/brainfuck | Formalizing Brainfuck in Coq to prove its properties and verify a compiler for simple arithmetic expressions. | 26 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
| coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
 thery/flocqlecture | An introductory course on floating-point numbers and formal proof using Coq | 6 |