The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

Hello,

I was looking for certified extractable depth-first-search and
strongly-connected-components construction algorithms in Coq. I found
two SCCs with decidable and termination proofs:
*  one is in the CoLoR project:
http://color.inria.fr/doc/CoLoR.Util.Relation.SCC_dec.html,
      The algorithm, for each pair of nodes, checks if a path exists.
Its complexity could be at least O(n*n).
*  the other is from http://www.lri.fr/~arnold/projects:coqgraphs
      based on adjacent matrix, the complexity could be O(n*n).
but, failed to find DFS proofs. Does anyone know if there are any DFS
proofs, or SCC proofs with less complexity?

Thanks
-- 
Jianzhou