The Coq contribution for Tarjan strongly connected component algorithm is composed of two files:
  1. extra_nocolors.v extends the Mathematical Components Library with some general purpose lemmas.
  2. tarjan_nocolors gives a more direct version of the proof with no notion of colours.
You can download the archive here.

If you want to execute these files, there are two solutions.

Installing Coq on your machine

You need Coq and the Mathematical Components Library installed on your machine

The contribution has been tested with version 8.9.0 and above of Coq and the version 1.7.0 of Mathematical Components Library.

The easiest way to install them, is to use the Ocaml installer opam

The instruction to install Coq via opam are given here.

Then you just need to do

opam install coq-mathcomp-fingroup

to get the part of the Mathematical Components Library that is needed.

Unzipping the archive and typing make inside the coq_tarjan directory should build the contribution.

Using your browser

Thanks to jscoq, you can directly browse and execute the contribution inside your favorite browser.
  1. extra_nocolors.v
  2. tarjan_nocolors.v
You can use the green buttons on the top right of the window to navigate into the script

NB: If your browser does not implement tail recursion optimisation for javascript (for example chrome), you may experience some problems with this solution.