Abstract Types in Distributed Systems

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 te 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.PARIS7-Bibliothèque centrale (751132105) / SudocSudocFranceF