Implementing hash-consed structures in Coq

Thomas Braibant, Jacques-Henri Jourdan, David Monniaux

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 includ…