Le 1er février 2010, à 13h30 (attention à l’horaire inhabituel !) en salle B311, le séminaire LCR accueille Paolo Tranquilli (ENS Lyon).

Les systèmes de types et effets permettent une analyse statique des effets de bord des programmes. Par exemple, en considérant la mémoire comme un ensemble de régions, on peut annoter le type d’une procédure qui accède à des variables globales avec l’ensemble des régions affectées. Récemment, des systèmes de types et effets à régions stratifiées ont été proposés pour assurer la terminaison de lambda-calculs avec références (partagées entre plusieurs threads).

Mon exposé partira d’un autre outil utilisé pour traiter les effets : les monades de Moggi sont une notion de théorie catégorique qui peut être utilisée en théorie des types pour "enrober" les effets en gardant le système "pur". La monade d’état TA = S → (S × A) permet de modéliser l’accès à la mémoire ; en outre, en paramétrant S avec les régions, on peut facilement traduire le lambda-calcul (séquentiel) avec types et effets dans le lambda-calcul avec paires. On arrive alors à une justification purement logique de la stratification : son absence est en fait équivalente au besoin d’utiliser des types récursifs.

La traduction se transfère aisément aux réseaux de preuve de la logique linéaire, à partir de la traduction du lambda-calcul par valeur (la deuxième traduction de Girard). Les réseaux donnent une réduction parallèle du calcul qui en préserve la sémantique séquentielle. On pourra alors passer au travail en cours, qui mène à étendre cette traduction au calcul multi-threaded en utilisant les réseaux différentiels. La traduction, qui utilise les zones de communications déjà exploité pour le pi-calcul, donne une simulation, mais les réseaux obtenus ne sont pas nécessairement corrects comme dans le cas séquentiel. On est donc obligé soit de restreindre le calcul concurrent, soit d’étudier des extensions des réseaux ou des modifications de leur critère de correction.