Modules
Current projects on modules:
Module Implicits
A formalization of OCaml modules
Some older work:
Open existentials