A verified system transformer for serialization of Verdi systems using the Cheerios library.
-
Updated
Aug 24, 2017 - Coq
A verified system transformer for serialization of Verdi systems using the Cheerios library.
Aniceto is a library that helps Coq development. It includes a libray of properties on graph theory.
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.
A library of mathematical structures based on type classes proposed in Haskell
Coq library that provides an abstract data type for environments [maintainer=@aerabi]
Archived since the contents have been moved to the topology repository
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
Strong non-interference for fine-grained concurrent programs
Library of useful utility functions for Coq plugins
A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
Formally verified algorithms in Coq: concepts and techniques
Coq
An mtl-like library for dealing with effects in Coq
Formalization of hashtables with Radix trees and PArray in Coq
Formally verified Coq serialization library with support for extraction to OCaml
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."