Skip to Main content Skip to Navigation

A module calculus enjoying the subject-reduction property. (Preliminary Version)

Abstract : The module system of SML is a small typed language of its own. As is, one would expect a proof of its soundness following from a proof of subject reduction, but none exists. As a consequence the theoretical study of reductions is difficult, and for instance, the question of normalization of the module calculus can not even be asked. In this paper, we build a variant of the SML module system --- inspired from recent works --- which enjoys the subject reduction property. This was the initial motivation. Besides our system enjoys other type-theoretic properties: the obtained calculus is strongly normalizing, there are no syntactic restrictions on module paths, it enjoys a purely applicative semantic, every module has a principal type, and type inference is decidable. Moreover we conjecture that type abstraction --- achieved through an explicit declaration of the signature of a module at its definition --- is preserved.
Document type :
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:12:23 AM
Last modification on : Thursday, November 21, 2019 - 2:38:44 AM


Files produced by the author(s)


  • HAL Id : hal-02102028, version 1



Judicael Courant. A module calculus enjoying the subject-reduction property. (Preliminary Version). [Research Report] LIP RR-1996-30, Laboratoire de l'informatique du parallélisme. 1996, 2+14p. ⟨hal-02102028⟩



Record views


Files downloads