Pierre hyvernat (LAMA, Université de Savoie)

foncteurs polynomiaux, jeux et logique linéaire (différentielle)

Résumé: Les « systèmes d'interaction » étaient à l'origine un moyen de représenter une notion de « jeux » en théorie des types. On obtient de cette manière une catégorie de jeux et de simulations qui modélise la logique linéaire différentielle. Fait assez surprenant, la dynamique ne joue aucun rôle dans la définition de composition des stratégies !

Cette notion de jeux existe sous des noms différents : « containers » (Ghani, Altenkirch, Hancock, ...) ou « foncteurs polynomiaux » (Hyland, Kock, Gambino, ...). Ce qui change ici est la notion plus générale de morphisme.

Après une petite introduction, je montrerai les liens entre ces polynômes (point de vue intentionnel) et les foncteurs associés (point de vue extensionnel). Je construirai ensuite le modèle de (D)ILL en insistant sur l'interprétation en termes de jeux et les similarités formelles avec le modèle « dégénéré » des transformateurs de prédicats.

Je ne ferai probablement aucune preuve, mais je mentionnerai quand même l'outil important, à savoir le langage interne des catégories localement cartésiennes fermées (càd la théorie des types dépendants)...