A library of mathematical structures based on type classes proposed in Haskell
-
Updated
Apr 4, 2020 - Coq
A library of mathematical structures based on type classes proposed in Haskell
A Coq library to embed Impure OCaml oracles in certified Coq code
Formalization of hashtables with Radix trees and PArray in Coq
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
Strong non-interference for fine-grained concurrent programs
A Coq library to embed Impure OCaml oracles in certified Coq code
Some personal notes on typical algebra topics
A verified system transformer for serialization of Verdi systems using the Cheerios library.
Solutions (in Coq) of the exercises in the software foundation books.
Aniceto is a library that helps Coq development. It includes a libray of properties on graph theory.
Coq library that provides an abstract data type for environments [maintainer=@aerabi]
Coq
A Coq tactic for proving multivariate inequalities using SDP solvers
An mtl-like library for dealing with effects in Coq
Formally verified algorithms in Coq: concepts and techniques
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.
Binary rational numbers in Coq [maintainer=@herbelin]
Add a description, image, and links to the coq-library topic page so that developers can more easily learn about it.
To associate your repository with the coq-library topic, visit your repo's landing page and select "manage topics."