tarjan
Graph algorithm formalization
Formalization of Tarjan and Kosaraju's strongly connected component algorithm in Coq for finite graphs.
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]
13 stars
8 watching
7 forks
Language: Coq
last commit: over 1 year ago
Linked from 1 awesome list
coqmathcompmathcomp-cissreflecttarjan-algorithm
Related projects:
| Repository | Description | Stars |
|---|---|---|
| coq-community/graph-theory | A comprehensive Coq library formalizing various results in graph theory, providing a rigorous foundation for theoretical and applied graph theory research. | 34 |
| coq-community/fourcolor | A formal proof of a fundamental result in graph theory using the Coq proof assistant | 166 |
| coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| coq-community/hydra-battles | Investigating various aspects of discrete mathematics and formal proofs in Coq, including ordinal numbers and computability theory. | 68 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 28 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| coq-community/alea | A library for reasoning about randomized algorithms in Coq | 25 |
| coq-community/topology | Develops and formalizes basic concepts and results of general topology in Coq. | 47 |
| coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
 geocoq/geocoq | A formalization of geometry using the Coq proof assistant. | 186 |
| coq-community/parseque | A Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq. | 42 |
| coq-community/coqtail-math | A collection of mathematical theorems and tools within the Coq proof assistant | 15 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |