Ssreflect
Showing 20 of 20 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 library providing Haskell-like definitions and notations for formalizing Haskell types and functions in Coq.
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 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.
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.
Coq lessons and exercises introducing the SSReflect proof language and Mathematical Components library.
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.