Commit e90f17d7 authored by charguer's avatar charguer
Browse files

cfml readme

parent fbe40b7d
......@@ -3,6 +3,10 @@
This is CFML 1.0, not to be confused with CFML 2.0.
CFML 1.0 is expected to be entirely subsumed by CFML 2.0 by the end of 2020.
CFML is a tool for carrying out proofs of correctness of OCaml programs with
respect to specifications expressed in higher-order Separation Logic.
......@@ -16,33 +20,36 @@ CFML consists of two parts:
to reason inside Coq about the code. In short, these tactics allow
the reasoning rules of Separation Logic to be applied to the OCaml code.
For related research papers, see:
The current version of CFML requires Coq 8.6 or newer.
The simplest way of installing the *latest released version* of CFML is via `opam`.
CFML 1.0 only works with Coq v8.8. Using OPAM, you might succeed in installing
CFML using the following commands.
# This only needs to be done once, to add the opam repository with coq packages
opam repo add coq-released
opam install coq-cfml
If instead you wish to use *the development version* of CFML,
then the last line above should be replaced by the following:
opam pin add coq-cfml
opam repo add coq-released
opam pin add coq-cfml
opam switch create coq_8.8.2 ocaml-base-compiler.4.07.0
opam pin add coq 8.8.2
opam install pprint ocamlformat coq coqide coq-tlc coq-cfml coq-aac-tactics.8.8.0
Getting started
Once CFML is installed, you can:
Once CFML is installed, you can replay the demo from the ICFP script.
git clone
cd cfml/examples/Tour
coqide MutableQueue_proof.v UFArray_proof.v
- Step through the tutorial. Clone the CFML git repository, then:
or play with files accompanying a tutorial on CFML.
cd cfml/examples/Tuto
......@@ -50,15 +57,13 @@ make
coqide Tuto_proof.v
- Use [cfml-skeleton]( to set up a
new project that uses CFML.
Some documentation can be found in doc/doc.html.
Some documentation is available in doc/doc.html.
Disclaimer: Pieces of it might be out of date.
Note that it is currently somewhat outdated and needs updating.
......@@ -68,4 +73,4 @@ All files are distributed under the GNU-GPL v3 license.
If you need a more permissive license, please contact the author.
Authors: Arthur Charguéraud,
with contributions from others.
with contributions from François Pottier and Armaël Guéneau.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment