Ulrich Schöpp

Coordinates

E-Mail
let X=schoepp in let A=tcs.lmu.ifi.de in X@A
GPG Key
Office Address
Raum D1.09
Theoretische Informatik
Oettingenstraße 67
D-80538 München
Germany
Office Phone
+49 89 2180 9309

A Formalised Lower Bound on Undirected Graph Reachability

Paper

A Formalised Lower Bound on Undirected Graph Reachability (Draft)

Formalisation in Coq

Browse the formalisation:
Summary of Main Results, JAGs and Reachability, General Index.

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.