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.0.tar.gz
sha256=abed66d36c76e0824f32322c9b951d5154203d98e3ee65943e30925da089e133

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

Published: 28 Oct 2021

Dependencies (1)

  1. coq-mathcomp-fingroup

Dev Dependencies (2)

  1. coq-mathcomp-ssreflect (>= "1.12.0" & < "1.14~") | (= "dev")
  2. coq (>= "8.10" & < "8.15~") | (= "dev")

Used by

None

Conflicts

None