Recursive Object-Oriented Module System

Abstract. ML-style modules and classes are complementary. The for-mer are better at structuring and genericity, the latter at extension and mutual recursion. We investigate the convergence of both mechanisms by designing an object-oriented calculus based on a nominal module system with mutual recursion. Our modules assume simultaneously the roles of classes with subtyping, nested structures with type members, and sim-ple functors. Flexible inter-module recursion is obtained by allowing free references not constrained by the order of definitions. We closely exam-ine the well-foundedness of the recursion, in the presence of nesting and functors. The presented type system is provably decidable, and ensures the well-foundedness. We also define a call-by-value semantics, for which type soundness is proved.