Depth-First Search and Strong Connectivity in Coq

Abstract : 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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/hal-01096354
Contributor : David Baelde <>
Submitted on : Wednesday, December 17, 2014 - 12:38:08 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Document(s) archivé(s) le : Monday, March 23, 2015 - 3:00:51 PM

File

jfla15_submission_2.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01096354, version 1

Collections

Citation

François Pottier. Depth-First Search and Strong Connectivity in Coq. David Baelde; Jade Alglave. Vingt-sixièmes journées francophones des langages applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. 〈http://jfla.inria.fr/2015〉. 〈hal-01096354〉

Share

Metrics

Record views

360

Files downloads

137