Séance Séminaire

Séminaire Algèbre Géométrie Algébrique Topologie Algébrique

Langages de programmation, substitution et multicatégories

L'étude et la conception des langages de programmation est profondément liée à des domaines mathématiques tels que la logique, la théorie des catégories, ou encore les théories algébriques. Cet exposé introduira tout d'abord un aperçu de ces interactions. La substitution est une opération subtile au cœur de l'étude des langages de programmation. Elle apparaît également en sémantique mathématique à travers la composition des catégories et en algèbre combinatoire, par exemple dans la théorie des opérades. Cet exposé se poursuivra par une présentation algébrique et catégorique de la substitution à l'aide de multicatégories et de monades dites de contexte. Les fonctions linéaires et non-linéaires, bien connues en mathématiques, ont leurs équivalents dans les langages de programmation. Dans un travail en collaboration avec Martin Hyland, nous avons montré que nous pouvions combiner les monades de la substitution linéaire et de la substitution non-linéaire afin de construire la monade de contexte nécessaire à la description de la substitution mixte linéaire/non-linéaire. Cet exposé se terminera par la présentation de ce résultat. À travers cet exposé, je montrerai comment la sémantique mathématique guide la conception de nouvelles constructions syntaxiques dans les langages de programmation et force l'étude de nouveaux concepts mathématiques.