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.
Type de document :
Communication dans un congrès
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>
Liste complète des métadonnées

https://hal.inria.fr/hal-01096354
Contributeur : David Baelde <>
Soumis le : mercredi 17 décembre 2014 - 12:38:08
Dernière modification le : jeudi 31 décembre 2015 - 01:03:59
Document(s) archivé(s) le : lundi 23 mars 2015 - 15:00:51

Fichier

jfla15_submission_2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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>

Partager

Métriques

Consultations de
la notice

236

Téléchargements du document

90