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