Une sémantique des jeux parallèle pour PCF
Pierre Clairambault
LIP, CNRS, ENS Lyon
http://perso.ens-lyon.fr/pierre.clairambault/
Date(s) : 30/06/2016 iCal
11h00 - 12h00
PCF est le langage paradigmatique pour la programmation séquentielle d’ordre supérieur. Mais bien que séquentiel, étant purement fonctionnel, son ordre d’évaluation ne peut être observé par un environnement pur.
L’évaluation de termes de PCF peut donc tirer parti du parallélisme, sans changer le résultat final. Cependant, la sémantique des jeux classique de PCF est incompatible avec cette évaluation parallèle. Dans un travail commun avec Castellan et Winskel, nous avons construit une interprétation de PCF plus relachée, où les stratégies sont des ordres partiels. Malgré ce parallélisme, notre modèle satisfait le même résultat de pleine adéquation que ceux classiques de HO et AJM.
Dans cet exposé, je commencerai par présenter une vision d’ensemble des différentes étapes du résultat. Ensuite, je ferai une introduction sur le cadre sémantique que nous utilisons pour interpréter les programmes par des structures d’événements. Je décrirai la catégorie compacte fermée des jeux concurrents, et montrerai comment y développer une version affine parallèle des jeux d’arènes. Si le temps le permet je montrerai comment gérer la réplication, et décrirai la catégorie cartésienne fermée et l’interprétation de PCF.
Catégories
