Formalizing OCaml modules

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

The general case, including applicative and generative functors, as well as transparent ascription Fulfilling OCaml modules with Transparent Existentials [ PDF ] has been submitted for publication.

A mode detailed, pedagogical description, but retricted the generative Retrofitting OCaml Modules [ PDF ] has been presented at JFLA 2023.