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. C
    Cyril Cohen <cyril.cohen@inria.fr>

Sources

1.0.1.tar.gz
sha256=4f79fe6f0f480b34026ce71936754478b90545cad35b0b04d9c45e93981cfc76

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

Published: 19 Jun 2023

Dependencies (3)

  1. coq-mathcomp-fingroup
  2. coq-mathcomp-ssreflect >= "1.12.0" & < "1.18~"
  3. coq >= "8.12" & < "8.19"

Dev Dependencies

None

Used by

None

Conflicts

None