Unique solution techniques for processes and functions
Institution:
LyonDisciplines:
Directors:
Abstract EN:
The bisimulation proof method is a landmark of the theory of concurrency and programming languages: it is a proof technique used to establish that two programs, or two distributed protocols, are equal, meaning that they can be freely substituted for one another without modifying the global observable behaviour. Such proofs are often difficult and tedious; hence, many proof techniques have been proposed to enhance this method, simplifying said proofs. We study such a technique based on ’unique solution of equations’. In order to prove that two programs are equal, we show that they are solution of the same recursive equation, as long as the equation has the ’unique solution property’: two of its solutions are always equal. We propose a guarantee to ensure that such equations do have a unique solution. We test this technique against a long- standing open problem: the problem of full abstraction for Milner’s encoding of the call-by-value λ-calculus in the π-calculus.
Abstract FR:
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.