Abstract:
Dans cet exposé, on s'intéresse aux catégories de réponse (des catégories avec les produits finis et un objet exponentiel, introduites par Selinger) sous deux aspects :
- un sous-ensemble du lambda-calcul simplement typé, qui engendre une catégorie de réponse libre,
- une sémantique à base de jeux graphiques, i.e., où les positions sont certains graphes vus comme des espaces topologiques, les coups des transformations de ces graphes, et les lambda-termes correspondent à certaines stratégies.
La composition usuelle des catégories provient de deux propriétés du jeu graphique :
- le recollement des stratégies, défini grâce à la topologie des positions, et qui s'interprète comme une composition parallèle,
- la descente de stratégies le longs de certains morphismes (coupures).
Le but est d'ébaucher une structure triple-catégorique pour décrire un langage de programmation, et de voir :
- une sémantique d'un langage comme un préfaisceau sur cette structure,
- une compilation comme un morphisme de triple-préfaisceaux.