Reseña: Depth-first search and strong connectivity in Coq
Se ha publicado un artículo de razonamiento formalizado en Coq sobre grafos titulado Depth-first search and strong connectivity in Coq.
Su autor es François Pottier (del grupo Gallium en el INRIA de Rocquencourt).
Su resumen es
Using Coq, we mechanize Wegener’s proof of Kosaraju’s linear-time algorithm for computing the strongly connected components of a directed graph. Furthermore, also in Coq, we define an executable and terminating depth-first search algorithm.
El trabajo se ha presentado en las Journées Francophones des Langages Applicatifs (JFLA 2015).
El código de las correspondientes teorías en Coq se encuentra aquí.