Retour
à la page du projet :Proposition de stage
Récemment introduit, le calcul bleu [1] propose une synthèse du lambda-calcul et du pi-calcul. Le premier est bien établi comme modèle de la programmation fonctionnelle, le second a l'ambition de jouer le même rôle vis à vis des systèmes distribués. Le stage proposé porte sur les techniques de preuve d'équivalence de ``programmes'' écrits dans le calcul bleu. Une telle équivalence, basée sur la notion de test, a été proposée dans [1], mais elle n'est pas particulièrement bien adaptée à la preuve d'égalités (ou d'inégalités) entre termes du calcul. On peut aussi définir très aisément une ``équivalence à barbes'' pour le calcul bleu, mais elle a le même défaut.Des travaux récents (référencés ci-dessous) ont montré que, pour des calculs proche du calcul bleu, il est possible de donner une caractérisation de l'équivalence à barbes, en termes de transitions étiquetées, qui fournit une technique de preuve très puissante. L'objectif du stage est, en s'appuyant sur les articles cités ci-dessous, de voir s'il est possible de donner une caractérisation analogue pour l'équivalence à barbes du calcul bleu. On peut d'ailleurs se poser aussi la même question pour l'équivalence observationnelle considérée dans [1].
Tels : 04 92 38 76 39 // 04 92 38 79 40
email :Ilaria.Castellani@sophia.inria.fr // Gerard.Boudol@sophia.inria.fr
Retour
à la page du projet :