This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
Updated
Sep 11, 2024 - Coq
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
A framework for formally verifying distributed systems implementations in Coq
Verified Software Toolchain
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Formalization of C++ for verification purposes.
A foundational framework for modular cryptographic proofs in Coq
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
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.
Partial Commutative Monoids
Formally verified Coq serialization library with support for extraction to OCaml
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
Binary rational numbers in Coq [maintainer=@herbelin]
Library of useful utility functions for Coq plugins
A Coq tactic for proving multivariate inequalities using SDP solvers
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."