coq-cfml

A tool for proving OCaml programs in Separation Logic CFML is a tool for carrying out proofs of correctness of OCaml programs with respect to specifications expressed in higher-order Separation Logic. CFML consists of two parts: - a tool, implemented in OCaml, parses OCaml source code and generates Coq files that contain characteristic formulae, that is, logical descriptions of the behavior of the OCaml code. - a Coq library exports definitions, lemmas, and tactics that are used 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.

opam install coq-cfml.20180525
homepage
https://gitlab.inria.fr/charguer/cfml
license
CeCILL-B
bugs tracker
https://gitlab.inria.fr/charguer/cfml/issues
dependencies
ocaml (>= 4.03.0 & < 4.07.0) & ocamlbuild & pprint & base-bytes & coq >= 8.6 & coq-tlc >= 20171206
source
https://gitlab.inria.fr/charguer/cfml/repository/20180525/archive.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-cfml/coq-cfml.20180525