This project is joint work with Clément Blaudeau and Gabriel Radanne.
Avoiding Signature Avoidance in ML Modules with Zippers. [ PDF ] Will be presented at POPL’25. This presents ZipML, a formalization of a large subset of OCaml module, using the OCaml-Style path-based approach, extended with zippers to delay the resolving of signature avoidance problems.
Fulfilling OCaml modules with Transparency [PDF | without appendices | appendices] accepted at OOPSLA’24. This presents Mω, a formalization of a large subsect of OCaml modules, including applicative and generative functors, as well as transparent ascription by elaboration in System Fω.
Retrofitting OCaml Modules [ PDF;
Extended
version ] has been presented at JFLA 2023.
This is a detailed, pedagogical description of OCaml modules, but
retricted the generative.