An Applicative Module Calculus

The SML-like module systems are small typed languages of their own. As is, one would expect a proof of their soundness following from a proof of subject reduction. Unfortunately, the subject-reduction property and the preservatype abstraction seem to be incompatible. As a consequence, in relevant module systems, the theoretical study of reductions is meaningless, and for instance, the question of normalization of module expressions can not even be considered. In this paper, we analyze this problem as a misunderstanding of the notion of module definition. We build a variant of the SML module system — inspired from recent works by Leroy, Harper, and Lillibridge — which enjoys the subject n property. Type abstraction — achieved through an explicit declaration of the signature of a module at its definition — is preserved. This was the initial motivation. Besides our system enjoys other type-theoretic properties: the calculus is strongly normalizing, there are no syntactic restric...

• Type: Conference
• Year: 1997
• Where: TAPSOFT
• Authors: Judicaël Courant
• Keywords: Module Systems, Relevant Module Systems, SML-like Module Systems, Software Engineering, TAPSOFT 1997