bedrock

bedrock copied to clipboard

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.4pl2.

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 (one of the two): (1) 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.

(2) Or: make cito (no need to run "make" beforehand) to make the Cito compiler.

To make executable Cito example programs, see 'Bedrock/Platform/Cito/README'. Also see the 'Examples', 'Platform', 'Platform/Cito', and 'Platform/Facade' subdirectories of 'Bedrock/', and their READMEs.