Modelisation des regions dans un pi-calcul avec groupe
Silvano Dal-Zilio


Dans cet exposé, nous portons un nouveau regard sur le calcul des régions de Tofte et Talpin en nous aidant d'un codage dans un pi-calcul typé avec groupes.

Dans un langage fonctionnel avec régions, les valeurs sont allouées dans des segments mémoires  déterminées à la compilation. Ces segments sont contrôlés suivant une politique de pile qui améliore sensiblement la gestion de la mémoire.  Ainsi, le calcul des régions a été utilisé avec succès comme langage intermédiaire dans l'implantation de ML-Kit, un
compilateur sans ramasse-miettes pour Standard ML.

La notion de groupes a été introduite dans le calcul des ambients typé de Cardelli, Ghelli, et Gordon. Dans ce calcul,  comme dans le pi-calcul que nous nous proposons d'utiliser,
chaque nom appartient à un groupe statiquement déterminé. Utilisé dans un système de types avec effets, les groupes permettent la vérification de certaines propriétés liées à la mobilité.

Notre codage précise la correspondance intuitive entre régions et groupes. Nous proposons, entre autre, une nouvelle formulation de la propriété de conservation du typage pour le calcul des régions. Notre codage nous permet aussi de prouver la correction de la gestion des régions. Ce résultat est prouvé à l'aide d'une nouvelle loi d'équivalence comportementale pour notre pi-calcul.