Implementing and reasoning about hash-consed data structures in Coq

Abstract : We report on four different approaches to implementing hash-consing in Coq programs. The use cases include execution inside Coq, or execution of the extracted OCaml code. We explore the different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of performances and guarantees. We use the running example of binary decision diagrams and then demonstrate the generality of our solutions by applying them to other examples of hash-consed data structures.
Keywords : Coq BDD Hash-consing
Liste complète des métadonnées

https://hal.inria.fr/hal-00881085
Contributeur : Thomas Braibant <>
Soumis le : jeudi 7 novembre 2013 - 14:33:49
Dernière modification le : jeudi 11 janvier 2018 - 06:14:33
Document(s) archivé(s) le : lundi 10 février 2014 - 11:36:03

Fichiers

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

Identifiants

  • HAL Id : hal-00881085, version 1
  • ARXIV : 1311.2959

Citation

Thomas Braibant, Jacques-Henri Jourdan, David Monniaux. Implementing and reasoning about hash-consed data structures in Coq. 2013. 〈hal-00881085v1〉

Partager

Métriques

Consultations de la notice

345

Téléchargements de fichiers

387