Skip to content

Formalization of Wigderson's graph coloring algorithm in Coq

License

Notifications You must be signed in to change notification settings

siraben/coq-wigderson

Repository files navigation

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.

About

Formalization of Wigderson's graph coloring algorithm in Coq

Topics

Resources

License

Stars

Watchers

Forks

Contributors 3

  •  
  •  
  •