The BEDROCK Coq library
Mostly automated verification of higher-order programs with higher-order separation logic, with a small trusted code base
http://plv.csail.mit.edu/bedrock/


This release requires Coq 8.4 (final released version, not a beta).

To build, run one of the following:
   make native
or
   make ltac
to select whether to use the OCaml or Ltac reification code, respectively.
By default, you get the Ltac version, which is _much_ slower (i.e., adds hours to the time to build the library and all examples serially), but avoids the need to load a plugin into Coq, which can be tricky to do on some platforms.

Then, just run:
   make
and go take a break while it runs for an hour or so (if you're lucky enough to have a new-ish machine). ;)  Using the '-j' switch for parallel build is highly recommended.

Also see the 'examples' and 'platform' directories and their READMEs.