coq-library
There are 36 repositories under coq-library topic.
UniMath/UniMath
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
uwplse/verdi
A framework for formally verifying distributed systems implementations in Coq
PrincetonUniversity/VST
Verified Software Toolchain
rocq-community/math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
rocq-community/corn
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
DistributedComponents/disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
bluerock-io/BRiCk
Formalization of C++ for verification purposes.
SSProve/ssprove
A foundational framework for modular cryptographic proofs in Coq
rocq-community/topology
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
imdea-software/fcsl-pcm
Partial Commutative Monoids
vafeiadis/hahn
Hahn: A Coq library
llee454/functional-algebra
This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
rocq-community/bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
uwplse/cheerios
Formally verified Coq serialization library with support for extraction to OCaml
uwplse/StructTact
Coq utility and tactic library.
rocq-community/coqoban
Sokoban (in Coq) [maintainer=@erikmd]
DistributedComponents/InfSeqExt
A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
PnVDiscord/PnVRocqLib
📝 A Rocq library written by members of PnV Discord Server
rocq-community/qarith-stern-brocot
Binary rational numbers in Coq [maintainer=@herbelin]
uwplse/coq-plugin-lib
Library of useful utility functions for Coq plugins
validsdp/validsdp
A Coq tactic for proving multivariate inequalities using SDP solvers
rocq-community/zorns-lemma
Archived since the contents have been moved to the topology repository
rocq-community/generic-environments
Coq library that provides an abstract data type for environments [maintainer=@aerabi]
boulme/Impure
A Coq library to embed Impure OCaml oracles in certified Coq code
co-dan/SeLoC
Strong non-interference for fine-grained concurrent programs
cogumbreiro/aniceto-coq
Aniceto is a library that helps Coq development. It includes a libray of properties on graph theory.
FedericoBruzzone/software-foundations
Solutions (in Coq) of the exercises in the software foundation books.
Eggy115/Coq
Coq
lukaszcz/sortalgs
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
valoran-M/diqt
Formalization of hashtables with Radix trees and PArray in Coq
wkolowski/coq-algs
Formally verified algorithms in Coq: concepts and techniques
wkolowski/coq-mtl
An mtl-like library for dealing with effects in Coq
boulme/ImpureDemo
A Coq library to embed Impure OCaml oracles in certified Coq code
DistributedComponents/verdi-cheerios
A verified system transformer for serialization of Verdi systems using the Cheerios library.
liyishuai/coq-show
The Show class in Coq