package coq-mathcomp-tarjan
Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp
Install
Dune Dependency
Authors
Maintainers
Sources
1.0.3.tar.gz
sha256=6f24af7801e560c819c48e562785b3145ef33666458cd8e014761e96b8bfced9
Description
This development contains formalizations and correctness proofs, using Coq and the Mathematical Components library, of algorithms originally due to Kosaraju and Tarjan for finding strongly connected components in finite graphs. It also contains a verified implementation of topological sorting with extended guarantees for acyclic graphs.
Tags
category:Computer Science/Graph Theory keyword:strongly connected components keyword:topological sorting keyword:Kosaraju keyword:Tarjan keyword:acyclicity keyword:graph theory logpath:mathcomp.tarjan date:2023-08-06Published: 10 May 2025
Dependencies (4)
-
coq-hierarchy-builder
>= "1.4.0" - coq-mathcomp-fingroup
-
coq-mathcomp-ssreflect
>= "2.0" & < "2.5~" -
coq
>= "8.16" & < "9.1~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page