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
Complete list of metadatas

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
Long-term archiving on : 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. Vingt-sixièmes journées francophones des langages applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01096354⟩

Share

Metrics

Record views

375

Files downloads

152