coq-library
There are 38 repositories under coq-library topic.
UniMath/UniMath
This coq 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
coq-community/math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
coq-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
bedrocksystems/BRiCk
Formalization of C++ for verification purposes.
SSProve/ssprove
A foundational framework for modular cryptographic proofs in Coq
coq-community/topology
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
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.
imdea-software/fcsl-pcm
Partial Commutative Monoids
uwplse/cheerios
Formally verified Coq serialization library with support for extraction to OCaml
coq-community/bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
coq-community/coqoban
Sokoban (in Coq) [maintainer=@erikmd]
uwplse/StructTact
Coq utility and tactic library.
DistributedComponents/InfSeqExt
A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
uwplse/coq-plugin-lib
Library of useful utility functions for Coq plugins
coq-community/qarith-stern-brocot
Binary rational numbers in Coq [maintainer=@herbelin]
validsdp/validsdp
A Coq tactic for proving multivariate inequalities using SDP solvers
coq-community/zorns-lemma
Archived since the contents have been moved to the topology repository
coq-community/generic-environments
Coq library that provides an abstract data type for environments [maintainer=@aerabi]
PnVDiscord/PnVRocqLib
A Coq library written by members of PnV Discord Server
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.
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.
FedericoBruzzone/software-foundations
Solutions (in Coq) of the exercises in the software foundation books.
motrellin/comoalg
Some personal notes on typical algebra topics