Formalizing Recursive Modules

This is the project dashboard for the INRIA / Didier Rémy Recursive Modules thread: OCaml recursive modules elaborated into an Mω / Fωμ-style target with equi-recursive types. Keep this separate from ISO-recursive Subtyping / weakly-positive subtyping.

Current focus

• POPL 2027 - OCaml Recursive Modules — active paper writing.
• Recursive Modules Paper Writing Log — chronological writing-progress tracker from diary and meetings.
• Latest meetings: May 12 - Meeting with Didier, May 5 - Meeting with Didier.
• Supporting mechanization: Fomega-rec formalization under Mechanization/.

Active todos

• Write Section 6 Related Work.
• Work out the source-to-source translation after Double Vision §4.4.
• Resolve and present the two Double Vision modes.
• Push recursive signature ^ww75 toward paper-ready formalization.
• Decide paper stance on head(π) ∉ fv(τ′) and k_equiv.
• Collect examples/proofs for lookup double vision and Opaque fallback.
• Follow up on Didier’s ZipML higher-kind check.

Paper and writing

• POPL 2027 - OCaml Recursive Modules
• Recursive Modules Paper Writing Log
• Story of formalizing recursive modules
• proposed rewriting for approximation
• Why we should keep head notin FV check in lookup applicative functors

Meetings

• May 12 - Meeting with Didier
• May 5 - Meeting with Didier

Mechanization / Fωμ

• Fomega-rec formalization
• Working logs live under Mechanization/Fomega-rec Formalization/Working Logs/.
• Treat this track as supporting material for the writing, not as the immediate main bottleneck.

Core technical notes

• Double Vision Problem - Abstract Types vs. Unconstrained Aliases in Recursive Modules
• Elaboration of Recursively Dependent Signatures
• Mutually Recursive Types in Recursive Modules
• Opacity Revisited in Recursive Modules
• Recursive type generativity
• OCaml type checking recursive modules
• Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types
• Cyclic type definitions in OCaml with opaque sealing

Literature / background

• What is a recursive module?
• Mixin modules
• Retrofitting and strengthening the ML module system
• A Syntactic Type System for Recursive Modules
• Recursive modules for programming
• A Type System for Recursive Modules
• A Formal Treatment of Recursive Modules in the M-omega Framework
• R1ML
• Jargon of Modules
• Singleton kinds

Older project notes

• Formalization of Recursive Modules
• Comparison of Formalizing Recursive Modules
• Initial Proposal of Formalization (Oct)
• Recursive Module Playground
• Recursive Module Discussion
• Fomega prototype implementation
• Fragements of Fomega
• Report generated by Gemini - Recursive Modules