Skip to main content

Examples

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

providing a translation in Coq of the economic 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.