Formalizing OCaml modules

This project is joint work with Clément Blaudeau and Gabriel Radanne.