d abstract) Keiko Nakata1 Jacques Garrigue2 1 Kyoto University Research Institute for Mathematical Sciences 2 Graduate School of Mathematics, Nagoya University The ML module system enables flexible development of large software systems by its support of nested structures, functors and signatures. In spite of this flexibility, however, recursion between modules is prohibited, since dependencies between modules must accord with the order of definitions. As a result of this constraint, programmers may have to consolidate conceptually separate components into a single module, intruding on modular programming. Recently much work has been devoted to extending the module system with recursion, and developing a type system for recursive modules has been one of the main subjects of study. Since recursion is an essential mechanism, one faces several issues to be considered for designing a practical type system. Our goal is to make recursive modules an ordinary construct for ML programmers. We w...