Équivalences comportementales typées dans le pi-calcul

We study the notion of program equivalences, i.e. proving that two programs can be used interchangeably without altering the overall observable behaviour. This definition is highly dependent on the contexts in which these programs can be used; does the context have exceptions, parallelism, etc… So proofs also need to be adapted according to the expressiveness of those contexts. This thesis presents on the pi-calculus – a concurrent programming language – under various typing constraints. Types allows us to impose different disciplines like forcing a sequential execution, or ensuring linearity, meaning an object can be used once. In each case, the bisimulation, a standard proof technique for the pi-calculus, needs to be adapted accordingly to obtain a suitable equivalence. We then test how using the modified bisimulations can be used to reason about a language with higher-order functions and references, which once translated into the pi-calculus satisfies the typing constraints.Nous étudions la notion d’équivalences entre programmes, c’est-à-dire prouver que deux programmes peuvent être utilisé de façon identique sans modifier le comportement global. Cette définition dépend beaucoup du contexte dans lequel ces programmes sont exécutés ; le contexte a-t-il accès à des exceptions, du parallélisme, etc… Ainsi, les preuves doivent être adaptées pour tenir compte des différents niveaux d’expressivité du contexte. Cette thèse s’intéresse au pi-calcul – un langage de programmation concurrent – sous différentes contraintes de typage. Ces types nous permettent de spécifier différentes disciplines comme imposer une exécution séquentielle du programme, ou encore assurer un comportement linéaire, c’est-à-dire que les objets ne peuvent être utilisés qu’une seule fois. Dans chaque cas, la bisimulation, une technique de preuve standard pour le pi-calcul, doit être adapté en conséquence afin d’obtenir une équivalence satisfaisante. Nous testons ensuite comment ces bisimulations modifiées peuvent être mise en pratique pour raisonner sur un langage avec des fonctions d’ordre supérieur et des références, langage qui une fois traduit dans le pi-calcul vérifie les contraintes de typage