math-comp / Fourcolor
Formal proof of the Four Color Theorem
Stars: ✭ 87
Labels
Projects that are alternatives of or similar to Fourcolor
Certint
A Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-55.17%)
Mutual labels: coq
Scala Escape
A compiler plug-in to control object lifetimes in Scala
Stars: ✭ 60 (-31.03%)
Mutual labels: coq
Formal Type Theory
Formalising Type Theory in a modular way for translations between type theories
Stars: ✭ 74 (-14.94%)
Mutual labels: coq
Typetheory
The mathematical study of type theories, in univalent foundations
Stars: ✭ 86 (-1.15%)
Mutual labels: coq
Silveroak
Formal specification and verification of hardware, especially for security and privacy.
Stars: ✭ 51 (-41.38%)
Mutual labels: coq
Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
Stars: ✭ 65 (-25.29%)
Mutual labels: coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-52.87%)
Mutual labels: coq
Disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Stars: ✭ 85 (-2.3%)
Mutual labels: coq
The Four Color Theorem
The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.
The formal proof is based on the Mathematical Components library for the Coq proof assistant.
Installation
If you already have OPAM installed:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-fourcolor
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].