thesis

Pi-calcul et sous-typage : inference de types et codages du lambda-calcul dans le pi-calcul

Defense date:

Jan. 1, 2000

Edit

Institution:

Paris 11

Disciplines:

Authors:

Directors:

Abstract EN:

Pas de résumé disponible.

Abstract FR:

Le pi-calcul est une algebre de processus definie a partir de deux concepts : nommer et communiquer. Les noms sont des canaux de communication, et communiquer consiste a echanger des noms. Le pi-calcul permet ainsi de representer des systemes concurrents dont les liens de communication peuvent evoluer dynamiquement. Le pi-calcul possede une grande puissance d'expression. On peut y coder diverses structures de donnees. Il permet de retrouver toute la puissance d'expression du lambda-calcul vu qu'on peut y coder ce dernier. On peut aussi y representer des objets et des objets concurrents ainsi que des calculs d'ordre superieur ou un processus peut etre transmis sur un canal. En utilisant comme seul mecanisme d'evaluation la communication, un langage noyau a ete bati directement sur le pi-calcul. Le pi-calcul a aussi servi de base pour definir de nouveaux calculs. Dans ce travail, nous nous interessons au sous-typage dans le pi-calcul. D'une part, nous definissons un systeme de types pi-sub, qui permet de specifier l'arite d'un canal et son mode d'utilisation : emettre uniquement, recevoir uniquement, emettre et recevoir ou est juste emis ou recu mais jamais utilise pour emettre ou recevoir. Nous proposons un algorithme d'inference de types pour ce systeme de types. Cet algorithme permet alors de detecter des erreurs de communication et de donner une analyse fine de l'utilisation des canaux. D'autre part, la possibilite de coder le lambda-calcul dans le pi-calcul, montre que ce dernier peut servir pour l'etude de la semantique de langages fonctionnels concurrents. Quand nous nous interessons aux langages types, etudier la correspondance entre le typage dans les deux calculs devient une question pertinente. Cela permet aussi de voir si des techniques developpees pour l'un peuvent etre utilisees pour l'autre. Nous etudions ce probleme en presence de sous-typage simple. Pour divers codages du lambda-calcul dans le pi-calcul, nous etudions la correspondance entre le typage dans lambda-sub et le typage dans pi-sub.