Mathematical Components
Showing 13 of 13 projects
A formal real analysis library for the Coq/Rocq proof assistant, built on the Mathematical Components library.
A Coq plugin providing high-level commands to declare and manage hierarchies of algebraic structures using packed classes.
A Coq library for effective algebra, providing optimized algorithms and a refinement framework for changing data representations in proofs.
A Coq library extending Mathematical Components with finite sets, finite maps, and multisets on choicetypes.
A Coq library providing verified translations between automata, regular expressions, and WS1S logic for regular languages.
Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.
A formal verification of the Feit-Thompson theorem (Odd Order Theorem) using the Coq proof assistant and Mathematical Components library.
Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.
A Rocq library providing stable mergesort algorithms with formal correctness proofs using relational parametricity.
Coq formalization and correctness proofs of Tarjan's and Kosaraju's algorithms for finding strongly connected components in graphs.
Coq lessons and exercises introducing the SSReflect proof language and Mathematical Components library.
Docker images providing stable versions of the Mathematical Components library for the Coq proof assistant.
A collection of formalized mathematical theories and algorithms extending the Mathematical Components library for Coq.
Related Tags
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.