Preuves algébriques dans le pi-calcul typé
Proposition de stage
Sujet:
Le pi-calcul [1] est un
calcul de processus qui est aux langages parallèles ce que le
lambda-calcul est aux langages fonctionnels (i.e. fondements, bases
théoriques).
Le pi-calcul typé est le noyau de langages
expérimentaux parallèles ou distribués comme Pict, Join,
et Facile.
La riche théorie algébrique et la théorie des types sont des
parties très important du pi-calcul, à la base de son succès
comme modèle du parallélisme. L'objectif principal
du projet est le développement d'un outil interactif pour prouver des
propriétés des processus du pi-calcul typé. Cet outil serait
développé préférablement en Java.
Le projet peut aussi comporter des développements de la théorie
algébrique et du systèmes de types du pi-calcul.
Après le Dea, ces travaux pourront être poursuivis en Thèse de
Doctorat, à priori dans le domaine des preuves algébriques
sur machine pour les
calculs ou langages parallèles à objets, comme Concurrent ML,
ML 2000, Java.
Contact:
Tels : 04 92 38 78 05 // 04 92 38 76 39
E-mails :
Davide.Sangiorgi@sophia.inria.fr
Laboratoire d'accueil:
Projets MEIJE, INRIA Sophia Antipolis
Prérequis:
Notions de pi-calcul appréciées, mais non nécessaires.
Connaissance, ou désir de connaissance de langage de programmation
Java.
Bibliographie:
[1] R. Milner. The polyadic pi-calculus: a tutorial.
Rapport de recherche de l'université d'Edinbourg ECS-LFCS-91-180.
Egalement proc. de la conf. Logic and Algebra of Specification,
Springer Verlag LNCS, 1993.
[2] B.Pierce and D. Sangiorgi.
Typing and subtyping for mobile processes,
(postscript file)
In Proc. eight annual IEEE Symposium on Logic in Computer Science (LICS
'93), IEEE Computer Society Press.
Version complète dans le journal MSCS 6(5), 409--454, 1996.
Retour
à la page du projet :
Retour
aux autres stages proposés dans le projet :
Last modified: Mon Oct 25 11:20:16 MET DST 1999