Abstract FR:

Cette thèse est une contribution au développement de modèles formels décrivant la migration de code. Plus particulièrement, nous y développons un calcul distribué fondé sur un fragment du π-calcul asynchrone dont la syntaxe est enrichie d'une distribution explicite des processus dans des localités et d'un opérateur de migration de processus entre différentes localités. Dans ce modèle, nous prouvons qu'une forme d'absence d'interblocage peut être garantie grâce à un système d'analyse statique simple combiné avec un système de types. Les canaux de communication ont une propriété dite de "réceptivité", et plus généralement nous démontrons la "livrabilité des messages" qui établit que tous les messages émis auront la possibilité d'être reçus, même éventuellement après migration. Une série d'exemples illustrant le "style de programmation réceptif", nous porte à croire que ce calcul distribué reste suffisamment expressif. La réceptivité peut également être exprimée dans le π-calcul asynchrone sans répartition. On démontre dans ce cas que la réceptivité n'est pas obtenue au détriment de son expressivité par un codage "fully-abstract" du π-calcul à récepteurs uniques dans le π-calcul réceptif. Pour cela, nous sommes amenés à développer des techniques de preuves de bisimulations asynchrones "up-to". Enfin, dans la dernière partie de cette thèse nous nous intéressons au problème de l'inférence de types pour le π-calcul réparti. Nous montrons que la présence de types dépendants complique ce problème et nécessite le développement de nouvelles techniques. Nous donnons un algorithme, qui, étant donné un terme du langage retourne les types les plus généraux. Nous montrons que cet algorithme est correct et complet.