mathcomp
There are 53 repositories under mathcomp topic.
math-comp/math-comp
Mathematical Components
math-comp/analysis
Mathematical Components compliant Analysis Library
rocq-community/fourcolor
Formal proof of the Four Color Theorem [maintainer=@ybertot]
ilyasergey/pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
math-comp/hierarchy-builder
High level commands to declare a hierarchy based on packed classes
DistributedComponents/disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
affeldt-aist/monae
Monadic effects and equational reasoning in Rocq
rocq-community/coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
affeldt-aist/infotheo
A Rocq formalization of information theory and linear error-correcting codes
rocq-community/autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
anton-trunov/csclub-coq-course-spring-2021
A course on formal verification at https://compsciclub.ru/en, Spring term 2021
math-comp/finmap
Finite sets, finite maps, multisets and generic sets
rocq-community/fav-ssr
Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]
rocq-community/reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
rocq-community/graph-theory
Graph Theory [maintainers=@chdoc,@damien-pous]
math-comp/algebra-tactics
Ring, field, lra, nra, and psatz tactics for Mathematical Components
math-comp/odd-order
The formal proof of the Odd Order Theorem
rocq-community/gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
arthuraa/extructures
Finite sets and maps for Coq with extensional equality
math-comp/Abel
A proof of Abel-Ruffini theorem.
math-comp/mczify
Micromega tactics for Mathematical Components
rocq-community/lemma-overloading
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
pi8027/stablesort
Stable sort algorithms and their stability proofs in Rocq
rocq-community/apery
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
rocq-community/bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
EngineeringSoftware/roosterize
Tool for suggesting lemma names in Coq verification projects
Yosuke-Ito-345/Actuary
Formalization of the basic actuarial mathematics using Coq
rocq-community/tarjan
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]
math-comp/multinomials
Multinomials for the Mathematical Components library.
math-comp/real-closed
Theorems for Real Closed Fields
rocq-community/regexp-Brzozowski
Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]
rocq-community/comp-dec-modal
Completeness and Decidability of Modal Logic Calculi [maintainer=@chdoc]
thery/grobner
A fornalisation of Grobner basis in ssreflect
validsdp/validsdp
A Coq tactic for proving multivariate inequalities using SDP solvers
EngineeringSoftware/math-comp-corpus
Corpus of Coq code related to MathComp including several machine-readable representations
math-comp/POPLmark
Solutions for the POPLmark challenge