package coq-mathcomp-tarjan
Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp
Install
Dune Dependency
Authors
Maintainers
Sources
1.0.4.tar.gz
sha256=077cc74998fc1acc5b3bb742c3936a7e497dbd37db23de71988ea86862518572
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: 13 Nov 2025
Dependencies (4)
-
coq-hierarchy-builder
>= "1.4.0" - coq-mathcomp-fingroup
-
coq-mathcomp-ssreflect
>= "2.0" & < "2.6~" -
coq
>= "8.16" & < "9.1~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page