Implementing hash-consed structures in Coq

DOI10.1007/978-3-642-39634-2_36MaRDI QIDQ5327368zbMATH OpenOpenAlexFDO

Authors Thomas Braibant, Jacques-Henri Jourdan, David Monniaux

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1304.6038

Mathematics Subject Classification ID

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.

Recommendations

• Implementing and reasoning about hash-consed data structures in Coq
• scientific article; zbMATH DE number 1696436
• scientific article; zbMATH DE number 2003158
• scientific article; zbMATH DE number 2061716
• Synthesis of ML programs in the system Coq

Cited in

(5)

• Importing HOL Light into Coq
• Program-ing finger trees in Coq
• On building cyclic and shared structures in Haskell
• Implementing and reasoning about hash-consed data structures in Coq
• scientific article; zbMATH DE number 1696436 (Why is no real title available?)

Describes a project that uses

Uses Software

• OCaml
• Coq

This page was built for publication: Implementing hash-consed structures in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327368)