Coq of OCaml Demos

Here we present some demos of the development version of coq-of-ocaml. Write at web [at] clarus [dot] me for more information. This work is currently made at Nomadic Labs. We use coq-of-ocaml to verify the implementation of Michelson, the language to write smart-contracts in the crypto-currency Tezos. Contributors needed!

Demos

Concepts

We import the purely functional part of OCaml to Coq. We aim to generate readable and idiomatic Coq code without encodings. The semantics of the source code may not be completely preserved. One should do manual reviews to assert that the generated Coq is a reasonable formalization of the sources. We generate a dummy Coq term and an explicit error message in case of error, so that we always generate something.

We compile OCaml projects by pluging into Merlin. This means that if you are using Merlin then you can run coq-of-ocaml with no additional configurations.

We do not do special treatments for the termination of fixpoints. We convert the code of the fixpoints, then  Coq may or may not validate the termination. It is possible to locally disable termination checks by installing the package coq-typing-flags from Simon Boulier (should be included in the comming Coq 8.11). We erase the type parameters for the GADTs. This makes sure that the type definitions are accepted, but can render the pattern matchings incomplete. We did not find a way to represent GADTs in Coq yet. Indeed, the dependent pattern matching works well on type indicies which are values, but not so well with types.

We support modules and first-class modules. We do not support functors. We generate either Coq modules or dependent records depending on the use case. We generate axioms for .mli files to help formalizations, but importing .mli files should be optional. We do not yet support cross-referencing between the generated Coq files.

Related projects

In the JavaScript community:

  • coq-of-js (under heavy development, contributors needed! sister project)

In the Haskell community: