Modèles des effets à base d'adjonction, et duploïdes

Le but de cet exposé est d'expliquer une nouvelle approche pour la modélisation des programmes avec effets, qui repose sur une caractérisation des modèles à base d'adjonction comme structures compositionnelles (duploïdes) dans lesquelles la composition vérifie des axiomes plus faibles que l'associativité, qui généralisent ainsi les catégories. À l'origine de cette approche est l'impossibilité de généraliser les algèbres de Boole sous la forme de catégories cartésiennes fermées avec objet dualisant, et la proposition de Girard (1992) de contourner cette impossibilité à travers un calcul des séquents classique dans lequel la règle de coupure n'est pas associative. Cette approche est généralisée aux logiques intuitionnistes et linéaires, et, du point de vue des programmes, à l'approche monadique des effets.