在Coq中实现hash consed结构
Implementing hash-consed structures in Coq
摘要：
我们报告三种不同的方法来使用散列consing与Coq系统认证的程序，使用二元决策图（BDD）作为运行的例子。用例包括在Coq内部执行，或执行提取的OCaml代码。在忠实使用原始提取代码和经过微调以使用Coq中不可用的OCaml编程结构的代码之间存在不同的权衡。我们讨论了性能和保证方面可能产生的后果。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
