GitHub - braibant/hash-consing-coq

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 21 Commits
bdd-reference		bdd-reference
extracted		extracted
figs		figs
pure		pure
smart		smart
Makefile		Makefile
README.txt		README.txt
bench_bdd.ml		bench_bdd.ml
bench_bdd.v		bench_bdd.v
pure.p.log		pure.p.log
pure.u.log		pure.u.log
ref-conservative.p.log		ref-conservative.p.log
ref-conservative.u.log		ref-conservative.u.log
ref.p.log		ref.p.log
ref.u.log		ref.u.log
script.ml		script.ml
shallow.p.log		shallow.p.log
shallow.u.log		shallow.u.log
smart.p.log		smart.p.log
smart.u.log		smart.u.log

Repository files navigation

Implementing hash-consed structures in Coq
==========================================

This is a public git repository associated with our submission to JAR. The Coq development and the OCaml handlers have been tested with Coq 8.4pl2 and OCaml 4.01. 

Description. 
============

pure/ contains two "pure" implementations of BDDs in Coq, and one implementation of reduction of hash-consed lambda-terms. 

smart/ contains the "smart" implementation of BDD in Coq, and one implementation of reduction of hash-consed lambda-terms. 

bdd-reference/ contains the reference implementation of BDDs by Filliâtre, that we use in our benchmarks

bench_bdd.{ml,v} corresponds to the frontend we used in our benchmarks. In order to generate the extracted code, please do "make all" from the root of the repository. This will compile and extract the pure-deep, pure-shallow and smart implementations.

script.ml contains the driver we used to to run our benchmarks. Execute it using "ocaml script.ml"