A Formalised Lower Bound on Undirected Graph Reachability
Formalisation in Coq
Download the formalisation sources:
reach1.1.zip (17 June 2008)
These files can be checked in Coq 8.1 with the tactic language extension SSReflect 1.1. A distribution of SSReflect 1.1 along with installation instructions can be obtained from the Mathematical Components Project.
A version of the proofs that can be checked with SSReflect 1.0 and Coq 8.0 is also still available: reach1.0.zip (last revision: Feb 2008). It also contains installation instructions for SSReflect 1.0.