Modular SMT Proofs for Fast Reflexive Checking inside Coq
Source code
Download the Coq development and Ocaml prover
[tgz]
, compiled with Ocaml 3.12 (
previous version
).
To run the benchmarks:
Install Ocaml 3.12, camlp5 and zchaff
Execute the following commands:
tar -zxf chk-no.tar.gz cd chk-no make make bench
For each benchmark, the script echos the Time Qed of Coq