Jeux concurrents à pointeurs et calcul à ressources
Date(s) : 04/12/2025 iCal
14h00 - 18h00
**Jury :**
Giulio Manzonetto, Professeur des universités, Université Paris Cité — Rapporteur
Guy McCusker, Professor of Computing, University of Bath — Rapporteur
Claudia Faggian, Chargée de recherche CNRS, Université Paris Cité — Examinatrice
Marie Kerjean, Chargée de recherche CNRS, Université Sorbonne Paris Nord — Examinatrice
Stefano Guerrini, Professeur des universités, Université Sorbonne Paris Nord — Président du jury
Lionel Vaux Auclair, Maître de conférences, Aix-Marseille Université — Directeur de thèse
Pierre Clairambault, Directeur de recherche, Aix-Marseille Université — Directeur de thèse
**Résumé :**
Cette thèse présente les jeux concurrents à pointeurs, et étudie les liens entre la
sémantique des jeux et le 𝜆-calcul à ressources.
On s’intéresse tout d’abord aux liens entre sémantique des jeux et modèle relationnel.
On commence par introduire un nouveau modèle de jeux, les jeux concurrents à pointeurs
(PCG). Ce modèle s’inspire à la fois des jeux HO traditionnels et des jeux concurrents.
On établit une bijection entre les augmentations (quotientées par isomorphisme) dans PCG
et les parties (quotientées par homotopie) des stratégies innocentes dans HO.
Ce modèle nous permet d’obtenir un premier résultat d’injectivité positionnelle dans PCG,
qui se traduit en un résultat d’injectivité positionnelle pour les stratégies innocentes,
finies et totales dans HO. On montre également que les stratégies innocentes partielles
infinies ne sont pas positionnellement injectives.
On introduit ensuite le calcul à ressources extensionnel, c’est-à-dire typé de façon à ce
que les termes en forme normale soient également en forme 𝜂-longue.
Ces termes sont en bijection avec les classes d’isomorphisme d’augmentations dans PCG.
On peut maintenant s’intéresser à l’aspect dynamique de la sémantique. On définit une
opération de composition dans PCG, et on montre que PCG est une catégorie symétrique
monoïdale fermée. La correspondance entre PCG et HO s’étend en un foncteur cartésien
fermé strict.
Pour étudier l’interprétation du calcul à ressources dans PCG, on cherche à exprimer plus
précisément sa structure catégorique. Pour cela, on introduit les catégories à ressources,
inspirées des catégories différentielles.
On définit l’interprétation du calcul à ressources dans une catégorie à ressources, et on
montre qu’elle est compatible avec la 𝛽-réduction. PCG forme une catégorie à ressources,
dans laquelle l’interprétation du calcul à ressources coïncide avec la bijection établie
précédemment pour les termes en forme normale.
Emplacement
Saint-Charles - FRUMAM (2ème étage)
Catégories
