/coq-wigderson

Formalization of Wigderson's graph coloring algorithm in Coq

Primary LanguageCoqMIT LicenseMIT

Towards the Formal Verification of Wigderson’s Algorithm

Created by: Ben Siraphob (siraben) and Jamison Homatas (jhomatas48)

We present progress towards the formal verification of Wigderson's graph coloring algorithm in Coq. We have created a library of formalized graph theory that aims to bridge the literature gap between introductory material on Coq and large-scale formal developments, while providing a motivating case study. Our library contains over 180 proven theorems.

Using Nix, run nix-shell then run make to compile it.

License

This software is licensed under the MIT license.