A module calculus enjoying the subject-reduction property. (Preliminary Version) - LARA - Libre accès aux rapports scientifiques et techniques Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1996

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

Résumé

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.
Le système de modules de SML est un vrai petit langage typé. Alors qu'on pourrait attendre une preuve de la consistance des systèmes de modules découlant de l'étude des réductions de modules, en particulier d'une preuve d'autoréduction, aucune preuve de ce genre ne semble exister. Or cela est un préliminaire nécessaire à toute étude des réductions, et en particulier à la question de la normalisation du système de modules. Dans ce rapport, nous construisons une variante du système de modules de SML, inspirée de travaux récents, qui possède la propriété d'autoréduction. Cette motivation initiale conduit par ailleurs à un système de modules possédant des propriétés théoriques remarquables: le calcul de modules est fortement normalisant, aucune restriction syntaxique sur les chemins d'accès n'est nécessaire, la sémantique de notre système est purement applicative, tout module possède un type principal, et l'inférence de type est décidable. Nous conjecturons par ailleurs que l'abstraction de type --- obtenue par un mécanisme de déclaration explicite de la signature d'un module lors de sa définition --- est préservée.
Fichier principal
Vignette du fichier
RR1996-30.pdf (225.95 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02102028 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02102028 , version 1

Citer

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⟩
20 Consultations
55 Téléchargements

Partager

Gmail Facebook X LinkedIn More