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. De manière assez surprenante, 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 de morphisme, plus générale que dans la littérature existante. Après une petite introduction, je montrerais les liens entre ces polynômes (point de vue intentionnel) et les foncteurs associés (point de vue extensionnel). Je construirais 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 ferais probablement aucune preuve, mais je mentionnerais 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)...