Mathcomp
Showing 23 of 23 projects
An extensive and coherent library of formalized mathematical theories built on the Coq/Rocq proof assistant with SSReflect.
A formal proof of the Four Color Theorem in Coq, including supporting theories for real numbers, plane topology, and combinatorial hypermaps.
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 Rocq library for formal reasoning about discrete probabilities, information theory, and linear error-correcting codes.
A Rocq library providing a formalized hierarchy of monads and their laws for monadic equational reasoning.
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/SSReflect port of the 'Functional Algorithms Verified' book, formalizing functional data structures and algorithms.
A Coq library providing verified translations between automata, regular expressions, and WS1S logic for regular languages.
A Coq library formalizing graph theory results, including Menger's Theorem, Hall's Marriage Theorem, and Wagner's Theorem.
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.
A Coq formalization of Bourbaki's Elements of Mathematics, covering set theory and number theory using the Mathematical Components library.
Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq's Hoare Type Theory.
A formal Coq development of the Tower of Hanoi problem with generalized frameworks and proofs.
A Rocq library providing stable mergesort algorithms with formal correctness proofs using relational parametricity.
A neural network-based tool that suggests lemma names for Coq verification projects by analyzing serialized statements and elaborated terms.
Coq formalization and correctness proofs of Tarjan's and Kosaraju's algorithms for finding strongly connected components in graphs.
Proof scripts and materials for tutorials on the Mathematical Components library and small-scale reflection in Coq.
Machine-checked constructive proofs of soundness, completeness, and decidability for modal logics K, K*, CTL, and PDL.
Docker images providing stable versions of the Mathematical Components library for the Coq proof assistant.
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.