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 :
Reports
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102028
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:12:23 AM
Last modification on : Thursday, November 21, 2019 - 2:38:44 AM

File

RR1996-30.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102028, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

12

Files downloads

13