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.20181201
homepage
https://gitlab.inria.fr/charguer/cfml
license
CeCILL-B
bugs tracker
https://gitlab.inria.fr/charguer/cfml/issues
dependencies
ocaml >= 4.03.0 & ocamlbuild & pprint & base-bytes & coq >= 8.6 & coq-tlc >= 20181116
source
https://gitlab.inria.fr/charguer/cfml/repository/20181201/archive.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-cfml/coq-cfml.20181201