#
Mathematical Components
Mathematical Components is a repository of formalized mathematics developed using
the Coq proof assistant. This project finds its roots in the formal proof of
the Four Color Theorem. It has been used for large scale formalization projects,
including a formal proof of the Odd Order (Feit-Thompson) Theorem.
Here are 47 public repositories matching this topic...
Lecture notes for a short course on proving/programming in Coq via SSReflect.
-
Updated
Jun 24, 2021 - Coq
Formal proof of the Four Color Theorem
-
Updated
Jun 8, 2021 - Coq
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
-
Updated
Oct 16, 2020 - Coq
Monadic effects and equational reasonig in Coq
monads
probabilistic-programming
monad-transformers
ssreflect
mathcomp
math-comp
nondeterminism
monadic-effects
-
Updated
Aug 4, 2021 - Coq
A Coq formalization of information theory and linear error-correcting codes
-
Updated
Aug 20, 2021 - Coq
A course on formal verification at https://compsciclub.ru/en, Spring term 2021
-
Updated
Aug 18, 2021 - HTML
Finite sets, finite maps, multisets and generic sets
-
Updated
Jun 11, 2021 - Coq
-
Updated
Aug 10, 2021 - Coq
A proof of Abel-Ruffini theorem.
-
Updated
Jun 7, 2021 - Coq
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
-
Updated
Jul 1, 2021 - Coq
The formal proof of the Odd Order Theorem
-
Updated
Jun 8, 2021 - Coq
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
-
Updated
Jul 11, 2021 - Coq
Finite sets and maps for Coq with extensional equality
-
Updated
Mar 4, 2021 - Coq
Tool for suggesting lemma names in Coq verification projects
-
Updated
Nov 23, 2020 - Python
Multinomials for the Mathematical Components library.
-
Updated
Aug 19, 2021 - Coq
Coq formalization of "A Decision Procedure for Regular Expression Equivalence in Type Theory" by Coquand and Siles [maintainer=@anton-trunov]
-
Updated
Oct 19, 2020 - Coq
Micromega tactics for Mathematical Components
-
Updated
May 13, 2021 - Coq
Experimental reflexive tactics for ring and field expressions
-
Updated
May 26, 2021 - Coq
Corpus of Coq code related to MathComp including several machine-readable representations
-
Updated
Jul 24, 2020 - Common Lisp
A Coq tactic for proving multivariate inequalities using SDP solvers
-
Updated
Jul 15, 2021 - Coq
Created by Georges Gonthier
Released 2008
Latest release 9 months ago
- Repository
- math-comp/math-comp
- Website
- math-comp.github.io