Ma thèse s’intéresse à la sémantique du pi-calcul – un langage de programmation concurrent – lorsqu’il est soumis à des contraintes de typage. L’objectif est de comprendre comment ces
restrictions affectent les bisimulations, des techniques de preuve existantes pour le pi-calcul. Ces équivalences typées, moins strictes, peuvent ensuite être exploitées pour raisonner sur d’autres langages via des traductions. Je me suis intéressé au lambda-calcul avec références comme langage source, en m’appuyant sur la traduction du lambda-calcul dans le pi-calcul proposée par Milner et raffinée par A. Durier, afin d’y ajouter les références. Cela a nécessité un travail préliminaire plus global sur le comportement des références dans le pi-calcul, présenté à CONCUR’20. Cette traduction est correcte, c’est-à-dire que si deux traductions sont équivalentes dans le pi-calcul, alors les programmes d’origine sont équivalents aussi. Cependant, la traduction n’est pas totalement abstraite au sens où la réciproque n’est pas vraie, d’où l’intérêt de considérer des équivalences typées, moins discriminantes. Pour cela, j’ai défini un système de types permettant de contraindre le pi-calcul à une exécution séquentielle en limitant le nombre de communications qui peuvent avoir lieu, et d’obtenir une notion de bon parenthésage entre processus : un processus en créant un autre doit terminer après le processus créé. Une notion de bisimulation bien-parenthésée a pu être ainsi définie et présentée à LICS’21. J’ai ensuite prouvé qu’une variante de cette technique donnait bien une traduction totalement abstraite pour le lambda-calcul avec références. Ce résultat sera présenté à ICALP’22.
Gratuit
Disciplines