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.