package coq-mathcomp-tarjan

  1. Overview
  2. No Docs
Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. C
    Cyril Cohen
  2. J
    Jean-Jacques Lévy
  3. K
    Karl Palmskog
  4. L
    Laurent Théry

Maintainers

  1. P
    palmskog@gmail.com

Sources

1.0.2.tar.gz
sha256=804d912cf8c30d63378a31df72349d83f3ef4e434c0adca7c34a25280d16ba49

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-06

Published: 06 Aug 2023

Dependencies (4)

  1. coq-hierarchy-builder >= "1.4.0"
  2. coq-mathcomp-fingroup
  3. coq-mathcomp-ssreflect >= "2.0"
  4. coq >= "8.16" & < "8.21~"

Dev Dependencies

None

Used by

None

Conflicts

None