Unique solution techniques for processes and functions

Techniques d'unicité des solutions pour processus concurrents et fonctions La méthode de preuve par bisimulation est un pilier de la théorie de la concurrence et des langages de programmation. Cette technique permet d’établir que deux programmes, ou deux protocoles distribués, sont égaux, au sens où l’on peut substituer l’un par l’autre sans affecter le comportement global du système. Les preuves par bisimulation sont souvent difficiles et techniquement complexes. De ce fait, diverses techniques ont été proposées pour faciliter de telles preuve. Dans cette thèse, nous étudions une telle technique de preuve pour la bisimulation, fondée sur l’unicité des solutions d’équations. Pour démontrer que deux programmes sont égaux, on prouve qu’ils sont solution de la même équation, à condition que l’équation satisfasse la propriété d’unicité des solutions : deux solutions de l’équation sont nécessairement égales. Nous utilisons cette technique pour répondre à une question ouverte, à savoir le problème de full abstraction pour l’encodage, dû à Milner, du λ-calcul en appel par valeur dans le π-calcul.