Abstract FR:

Cette these propose un modele de la programmation des systemes repartis. Elle presente le join-calcul, en developpe la theorie, et l'utilise comme noyau d'un langage de programmation. Le join-calcul est un calcul de processus asynchrone avec mobilite de nom. Il peut egalement etre interprete comme une extension parallele d'un petit langage fonctionnel. Sa semantique operationnelle est definie en termes de machines chimiques abstraites, de maniere a decrire une implementation repartie. Par construction, chaque etape du calcul peut s'implementer par l'envoi d'au plus message sur un reseau asynchrone, quelle que soit la repartition du calcul a l'execution. En premiere approximation, la localisation des ressources est donc transparente. Nous explorons plusieurs raffinements du modele, en ajoutant des primitives permettant de controler dynamiquement le placement des ressources et de modeliser des pannes partielles. Nous considerons diverses notions d'equivalence entre processus adaptees aux systemes asynchrones. Ces equivalences sont structurees en une hierarchie dont chaque echelon correspond a un compromis entre finesse de l'equivalence et complexite des preuves. Nous utilisons ces equivalences pour etablir la correction de codages internes au join-calcul, et entre le join-calcul et le pi-calcul.