package coq-mathcomp-tarjan
Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp
Install
Dune Dependency
Authors
Maintainers
Sources
1.0.5.tar.gz
sha256=90d00f0b3c550d90b1e80d24a1eecd4c2efe31381271a0cd59da2b302c7352e1
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: 24 Jul 2026
Dependencies (5)
-
coq-hierarchy-builder
>= "1.4.0" - coq-mathcomp-fingroup
-
coq-mathcomp-ssreflect
>= "2.0" & < "2.7~" -
rocq-core
>= "9.0" & < "9.3~" -
coq
>= "8.16" & < "8.21~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page