#

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 50 public repositories matching this topic...

math-comp / math-comp

Mathematical Components

coq ssreflect mathcomp

Updated Nov 14, 2022
Coq

math-comp / analysis

Mathematical Components compliant Analysis Library

analysis coq ssreflect mathcomp

Updated Nov 16, 2022
Coq

ilyasergey / pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.

dependent-types tutorial coq hoare-logic ssreflect mathcomp

Updated Jun 24, 2021
Coq

coq-community / fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

coq ssreflect four-color-theorem mathcomp

Updated Nov 15, 2022
Coq

DistributedComponents / disel

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

distributed-systems coq proof separation-logic coq-library two-phase-commit ssreflect mathcomp

Updated Oct 16, 2020
Coq

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes

coq mathcomp elpi

Updated Nov 4, 2022
Prolog

affeldt-aist / monae

Monadic effects and equational reasonig in Coq

monads probabilistic-programming monad-transformers ssreflect mathcomp math-comp nondeterminism monadic-effects

Updated Nov 16, 2022
Coq

coq-community / coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

coq refinement mathcomp

Updated Aug 24, 2022
Coq

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes

information-theory probability error-correcting-codes ssreflect mathcomp math-comp convexity

Updated Nov 16, 2022
Coq

anton-trunov / csclub-coq-course-spring-2021

A course on formal verification at https://compsciclub.ru/en, Spring term 2021

course coq ssreflect mathcomp

Updated Aug 18, 2021
HTML

math-comp / finmap

Finite sets, finite maps, multisets and generic sets

coq ssreflect finite-sets mathcomp

Updated Nov 16, 2022
Coq

coq-community / autosubst

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

coq variable-binding ssreflect debruijn-indices mathcomp

Updated Sep 5, 2022
Coq

coq-community / reglang

Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]

regexp coq regular-languages ssreflect mathcomp docker-coq-action nix-action coq-platform

Updated Nov 13, 2022
Coq

math-comp / Abel

A proof of Abel-Ruffini theorem.

coq ssreflect galois-theory mathcomp abel-ruffini

Updated Oct 30, 2022
Coq

arthuraa / extructures

Finite sets and maps for Coq with extensional equality

coq ssreflect finite-sets mathcomp

Updated Aug 9, 2022
Coq

coq-community / graph-theory

Graph Theory [maintainers=@chdoc,@damien-pous]

coq graph-theory mathcomp

Updated Aug 11, 2022
Coq

math-comp / algebra-tactics

Ring and field tactics for Mathematical Components

coq proof-automation ssreflect mathcomp elpi

Updated Nov 15, 2022
Coq

coq-community / lemma-overloading

Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]

automation coq typeclasses ssreflect paper-artifacts canonical-structures mathcomp

Updated Jan 20, 2022
Coq

coq-community / gaia

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

coq set-theory ssreflect mathcomp docker-coq-action bourbaki

Updated Aug 12, 2022
Coq

math-comp / odd-order

The formal proof of the Odd Order Theorem

coq ssreflect mathcomp odd-order-theorem feit-thompson-theorem

Updated Aug 31, 2022
Coq

Created by Georges Gonthier

Released 2008

Latest release 5 months ago

Repository: math-comp/math-comp
Website: math-comp.github.io