Implementing and reasoning about hash-consed data structures in Coq

DOI10.1007/s10817-014-9306-0zbMath1314.68273arXiv1311.2959OpenAlexW3104118861MaRDI QIDQ2351422

Thomas Braibant, David Monniaux, Jacques-Henri Jourdan

Publication date: 23 June 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

binary decision diagrams\texttt{Coq}hash-consing

Mathematics Subject Classification ID

Related Items (1)

Hash consed points-to sets

Uses Software

• ACL2
• Coq
• Haskell
• OCaml
• HimML
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Imperative Functional Programming with Isabelle/HOL
• Subset Coercions in Coq
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Characteristic formulae for the verification of imperative programs
• Adjustable References
• Theorem Proving in Higher Order Logics
• Extending Coq with Imperative Features and Its Application to SAT Verification

This page was built for publication: Implementing and reasoning about hash-consed data structures in Coq