This project consists of a series of experiments of verifying OCaml code in Coq.
Once you have installed the requirements, build the programs and their proofs with dune:
opam exec -- dune build @all
- Coq-cfml >= 20220112
- OCaml
Once you have the coq-repositories added:
opam repo add coq-released https://coq.inria.fr/opam/released
Simply install cfml:
opam install cfml coq-cfml
.
├── lib OCaml code
├── proofs Coq proofs
├── dune-project
└── Readme.md
3 directories, 2 files