My PhD thesis (in English, with an extended abstract in French). [.pdf].
Résumé : La présente thèse étudie les théories à la base de la mobilité, dans le but de développer des outils mathématiques de formalisation et de preuve des propriétés des systèmes mobiles.Afin de comprendre l'impact de la mobilité sur la théorie équationelle des langages, nous nous sommes intéressé à deux calculs de processus présentant deux modèles de mobilité opposés : le Seal Calcul et les Ambients Mobiles. Dans les deux cas, nous avons donné une caractérisation coinductive de l'équivalence observationnelle, ce qui a permis non seulement de développer des techniques puissantes de preuves de l'équivalence de deux systèmes, mais a aussi mis en relief certaines spécificités des deux modèles de mobilité. Dans le cas des Ambients Mobiles, la caractérisation est complète : ce résultat important a nécessité l'élaboration de techniques spécifiques permettant de manipuler la mobilité asynchrone et le stuttering. De plus, pour la première fois dans le cas de calculs d'ordre supérieur, on a démontré que des techniques de preuve dites up-to sont correctes.
En parallèle, nous avons pris les catégories de pré-faisceaux comme modèle de la concurrence, et nous avons donné une lecture operationelle d'une catégorie de pré-faisceaux appropriée pour modéliser la création de noms et les processus d'ordre supérieur. Cela nous a conduit à la définition d'un langage concis mais expressif, nommé new-HOPLA, à même de représenter une grande variété de langages de processus. Le langage est typé, et le type d'un terme décrit la forme des chemins d'exécution qu'il peut réaliser. Il a donc fallu élaborer le typage du langage, ce qui a été compliqué par la nécessité de distinguer les noms inédits des autres, ainsi que sa théorie opérationnelle. Nous avons en outre montré comment new-HOPLA peut être utilisé pour donner une sémantique à des calculs de processus comme le pi-calcul et les Ambients Mobiles.
Summary: This PhD dissertation addresses the theories underlying the mobile computation, with the aim to develop mathematical tools to express and reason about mobile systems.
We studied the impact that mobility of active computations has on the observational congruence, and in general on the equational theory of a process language. In particular, we focused on two process calculi, namely the Seal Calculus and the Ambient Calculus, that offer two opposite models of mobile computation. In both cases, we found a coinductive characterisation of observational congruence: these results not only originate powerful proof methods to prove the equivalence of two systems, but also highlight peculiarities of the two models of mobility. In the case of the Ambient Calculus, the characterisation is complete: this important result required the development of techniques to deal with asynchronous mobility and ``stuttering'' phenomena. Also, we showed the soundness of up-to proof techniques in the presence of higher-order computation.
We also studied presheaf categories as a general model of concurrency. We gave an operational reading of a presheaf category suitable to describe higher-order process and name generation. This led us to a compact but expressive language, called new-HOPLA, that directly encodes a rich variety of process languages. The language is typed, and the type of a term describes the shape of the computation paths it can perform. The operational theory of the metalanguage has also been developed, and the resulting operational equivalence theory has been investigated. The metalanguage has been used to give semantics to rich process algebras like pi-calculus and Mobile Ambients.
Soutenance: Thèse soutenue le 12 décembre 2003 à l'École normale supérieure (salle Beckett), devant le jury composé par Pierre-Louis Curien (président), Giuseppe Castagna, Matthew Hennessy, Jean-Jacques Lévy, Glynn Winskel. Rapporteurs : Matthew Hennessy et Davide Sangiorgi. Mention Très Honorable.