Soit un réseau de machines exécutant des programmes ML qui
s'échangent des données. Comment peut-on garantir le typage des
communications en présence de types abstraits ? Une approche
sûre est de traiter des types abstraits définis sur des machines
différentes comme distincts. En pratique, cela est bien trop
restrictif, en particulier lorsqu'un type abstrait sert à garantir
un invariant.

Les principales contributions de cette thèse sont les
suivantes : je définis une notion d'empreinte de type
abstrait : deux types abstraits sont réputés compatibles
s'ils ont la même empreinte ; je propose une sémantique
opérationnelle pour un système de module qui préserve les
types, y compris abstraits ; je décris un système de module
nouveau, mieux adapté aux applications réparties.

L'empreinte d'un type abstrait doit refléter sa sémantique
attendue, qui n'est pas toujours apparente au vu du code source. Une
approximation sûre est de donner la même empreinte à deux
modules lorsqu'ils ont le même code. Des modules composés sont
compatibles si leurs composants le sont.

Les sémantiques opérationnelles habituelles des modules de ML
effacent les barrières d'abstraction. J'utilise des crochets
colorés qui matérialisent ces barrières et évitent la
perte d'information. J'étudie deux calculs ainsi équipés, un
lambda-calcul simplement typé et un système de module expressif
pour ML.

J'exprime des équivalences de modules de signature arbitraire, pas
seulement de types, au moyen de signatures singleton. Un système
d'effets simple préserve le typage statique et permet de distinguer
des foncteurs applicatifs et génératifs. Je discute de formes
statiques et dynamiques du scellage de modules.