@Christian Doczkal so it seems like Graph Theory could be the place for a lot of proof-oriented graph theory. For example, do you think the work on strongly connected components (https://github.com/CohenCyril/tarjan) would fit there after some adaptation? Or how do you want to scope the project?

personally, I would find it useful to only have to depend on MC + Graph Theory for work in this direction (e.g., when writing practical verified code using topological sorts and the like)

One, lightly depressing, observation has been that the verification of graph algorithms (in particular the verification of intricate algorithms for easy to define concepts) does not profit much from a graph theory library. There often is little graph-theory knowledge required.

Moreover, the specific paper you mention chooses to verify the algorithm at the level of the original Why3 proof, not necessarily making the best use of the higher-order nature of Coq (or Isabelle). I had a chat with Stephan Merz about this, when they presented the paper.

OK, so you think the best way the community could maintain graph algorithm formalizations would be as a separate project?

I wouldn't state it in those absolute terms. It depends on the algorithm. If the existence of an algorithm is not completely obvious and the verification requires some graph theory insights, then there may well be a case do develop the algorithm on top of the graph theory library or even within.

My example would be a function computing a minimum-width tree-decomposition for a graph. Currently there is no lemma in the library that allows things like "let (T,B) be a minimum-width tree decomposition", because the existence of such a decomposition is not entirely obvious (and was so far not needed).

Last updated: Jul 25 2024 at 15:02 UTC