coq-mathcomp-tarjan.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
version: "dev"

homepage: "https://github.com/coq-community/tarjan"
dev-repo: "git+https://github.com/coq-community/tarjan.git"
bug-reports: "https://github.com/coq-community/tarjan/issues"
license: "CECILL-B"

synopsis: "Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp"
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."""

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.16"}
  "coq-mathcomp-ssreflect" {>= "2.0"}
  "coq-mathcomp-fingroup" 
  "coq-hierarchy-builder" {>= "1.4.0"}
]

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"
]
authors: [
  "Cyril Cohen"
  "Jean-Jacques Lévy"
  "Karl Palmskog"
  "Laurent Théry"
]