Examples

The main project handled with coq-of-ocaml is the crypto-currency Tezos. The result is in the project:

• coq-tezos-of-ocaml: https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/

providing a translation in Coq of the economic protocol of Tezos. You can also look at the historical result of the first compiling translation of the protocol of Tezos.

We are now focusing on:

• maintaining the translation of the protocol of Tezos, as the protocol evolves;
• improving this translation by removing some (supposedly safe) axioms;
• applying coq-of-ocaml to other OCaml programs.