During our work on verification of Tezos source code,
we run into an interesting question: how to implement OCaml's `GADTs`

in Coq?
The essence of this problem, as well as its solution, were described in
the article: Translating the Michelson interpreter
where we show how we introduce casts in the generated Coq code.

In this article, we will consider subsequent work in this direction.
To reach one of our main goals, proof of the compatibility of the parsing
and unparsing functions for the Michelson types and values,
we need to avoid `casts`

. A powerful Coq's instrument, the dependent types, will help
us to solve the `casts`

problem. We create a kind of clone of `coq-of-ocaml`

's
code, which is a dependently typed version.

The whole process can be structured as follows:

- the
`Simulations`

folder (along with its purpose and content), - definition of dependent types,
- definition of functions with dependent types (analogs of functions with casts),
- proof of the equivalence between functions with dependent types and functions with casts,
- proof of assertions and properties for functions with dependent types.

and this is how it is all organized in the repository:

- we keep files, generated by
`coq-of-ocaml`

in folder`Proto_alpha`

- we keep dependently-defined types and functions in folder
`Simulations`

- we keep our proofs in folder
`Proofs`