Implementing hash-consed structures in Coq

International audience

Data and Resources

Additional Info

Field Value
Source Interactive Theorem Proving
Author Braibant, Thomas, Jourdan, Jacques-Henri, Monniaux, David
Maintainer CCSD
Last Updated May 11, 2026, 08:57 (UTC)
Created May 11, 2026, 08:57 (UTC)
Identifier hal-00816672
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Programming languages, types, compilation and proofs (GALLIUM) ; Inria Paris-Rocquencourt ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
coverage Rennes, France
creator Braibant, Thomas
date 2013-07-22T00:00:00
harvest_object_id 41941606-43a4-405a-b5af-866d5eb337c7
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2026-04-28T00:00:00
relation info:eu-repo/semantics/altIdentifier/arxiv/1304.6038
set_spec type:COMM