Title: a calculus of call-by-value mixin modules

Abstract: 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 [1] and Wells and Vestergaard [3]
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 [2] 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 MMM, a call-by-value
calculus of mixin modules, with an untyped reduction semantics.  A
type system is formalized and proved sound.

[1] D. Ancona and E. Zucca, A calculus of module systems, JFP 2002.
[2] T. Hirschowitz and X. Leroy, Mixin modules in a call-by-value setting, 
    ESOP 2002.
[3] J.B. Wells and R. Vestergaard, Equational reasoning for linking 
    with first-class primitive modules, ESOP 2000.