Some personal notes on typical algebra topics
-
Updated
Jun 2, 2024 - Coq
Some personal notes on typical algebra topics
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Formalization of C++ for verification purposes.
Verified Software Toolchain
A framework for formally verifying distributed systems implementations in Coq
Partial Commutative Monoids
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]
A foundational framework for modular cryptographic proofs in Coq
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
A Coq tactic for proving multivariate inequalities using SDP solvers
A Coq library to embed Impure OCaml oracles in certified Coq code
A Coq library to embed Impure OCaml oracles in certified Coq code
Solutions (in Coq) of the exercises in the software foundation books.
Binary rational numbers in Coq [maintainer=@herbelin]
Formally verified Coq serialization library with support for extraction to OCaml
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Formalization of hashtables with Radix trees and PArray in Coq
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."