Soutenance de thèse de BLONDEAU-PATISSIER Lison
Titre de thèse
Jeux concurrents à pointeurs et calcul à ressources
Pointer Concurrent Games and the Resource Calculus
Résumé de la thèse
Cette thèse présente les jeux concurrents à pointeurs, et étudie les liens entre la sémantique des jeux d'une
part et le 𝜆-calcul à ressources d'autre part.
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.
Thesis resume
This thesis presents the Pointer Concurrent Games model. We study the links between game semantics and
resource 𝜆-calculus.
First, we focus on the links between game semantics and relational semantics. We introduce a new game
model, pointer concurrent games (or PCG), inspired by traditional HO games and by concurrent games. There is
a bijection bewteen augmentations (up to isomorphism) in PCG and plays (up to homotopy) of innocent strategies
in HO. We obtain a first result of positional injectivity in PCG, which translates to a result of positional
injectivity for total finite innocent strategies in HO. We also prove that partial infinite innocent strategies are not
positionaly injective.
Next we introduce the extensional resource calculus, i.e. a typed resource calculus where typing rules ensure
that terms in normal form are also in 𝜂-long form. These terms are in bijection with the augmentations (up to
isomorphism) in PCG.
We can now consider the dynamic aspect of the semantics. We define the composition in PCG, and we show
that PCG is a closed symetric monoidal category. The correspondance between PCG and HO is extended to a
strict cartesian closed functor.
Finally, in order to study the interpretation of the resource calculus in PCG, we try and describe more precisely
its categorical structure by introducing resource categories – inspired by differential categories. We construct
a sound interpretation of the resource calculus in a resource category, and we show that PCG is indeed a
resource category. Moreover, this interpretation coincides with the bijection for normal resource terms.