Categories and String Diagrams for Game Semantics

Catégories et diagrammes de cordes pour les jeux concurrents La sémantique des jeux est une approche pour modéliser les langages de programmation dans laquelle les types sont interprétés par des jeux et les programmes par des stratégies. Ces modèles de jeux ont couvert des constructions fonctionnelles et impératives, des opérateurs de contrôle, etc. L'approche a récemment été étendue aux langages non-déterministes et concurrents, provoquant au passage un changement de perspective profond~: les parties sont maintenant organisées en une catégorie, sur laquelle les stratégies sont des préfaisceaux. La notion fondamentale d'innocence a aussi été caractérisée comme une condition de faisceau. Cette thèse s'attache à l'étude de quelques constructions apparaissant dans ces nouveaux modèles de jeux.D'abord, constatant que, dans plusieurs de ces modèles, l'étape cruciale consiste à définir une catégorie double de jeux et de parties, nous proposons une construction abstraite d'une telle catégorie double à partir de données de base, puis nous démontrons que, sous des hypothèses adéquates, le résultat obtenu permet en effet la construction des stratégies.Dans un second temps, nous établissons un lien entre deux techniques existantes pour définir les parties~: la technique standard, fondée sur les séquences justifiées, et une autre plus récente utilisant les diagrammes de cordes. Nous définissons un plongement (plein) de la première dans la seconde et prouvons qu'elles induisent essentiellement le même modèle.Enfin, nous proposons une axiomatisation des notions de jeu et de partie, de laquelle nous tirons une catégorie de jeux et stratégies. Nous raffinons ensuite les axiomes pour traiter l'innocence et nous démontrons que, sous des hypothèses adéquates, les stratégies innocentes sont stables par composition.