||The ML module system provides powerful parameterization facilities, but lacks the ability to split mutually recursive definitions across modules, and does not provide enough facilities for incremental programming. A promising approach to solve these issues is mixin modules. Ancona and Zucca  and Wells and Vestergaard  have studied mixin modules calculi in a call-by-name setting. However,
the straightforward way to adapt it to ML fails, because arbitrary recursive definitions may appear at any time, which ML does not support. Hirschowitz and Leroy  have formalized a language of call-by-value mixin modules, whose semantics is given by type-directed translation down to a call-by-value lambda-calculus extended with a non-standard "let rec" construct. This presentation makes equational
reasoning difficult and prevents mixin modules to be first class entities in the language. We present MM, a call-by-value calculus of mixin modules, with an untyped reduction semantics. A type system is
formalized and proved sound.
 D. Ancona and E. Zucca, A calculus of module systems, JFP 2002.
 T. Hirschowitz and X. Leroy, Mixin modules in a call-by-value setting,
 J.B. Wells and R. Vestergaard, Equational reasoning for linking
with first-class primitive modules, ESOP 2000.