Implementing hash-consed structures in Coq
Programming Languages
2013-04-23 v1 Logic in Computer Science
Abstract
We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases include execution inside Coq, or execution of the extracted OCaml code. There are 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.
Cite
@article{arxiv.1304.6038,
title = {Implementing hash-consed structures in Coq},
author = {Thomas Braibant and Jacques-Henri Jourdan and David Monniaux},
journal= {arXiv preprint arXiv:1304.6038},
year = {2013}
}