Logique linéaire, Sémantique dénotationnelle, Bicatégories, Orthogonalité

Cette thèse porte sur la sémantique bicatégorique de la logique linéaire. Elle s'incrit dans le cadre de catégorification des modèles de calculs où l'on remplace des sémantiques où les types sont interprétés par des ensembles ou des préordres par des structures catégoriques plus riches permettant d'obtenir des invariants mathématiques plus fins. Nous nous intéressons spécifiquement à la catégorification du modèle relationel de la logique linéaire par le modèle des espèces généralisées introduit par Fiore, Gambino, Hyland et Winskel ansi qu'à ses raffinements par des constructions d'orthogonalité. Nous présentons dans un premier temps une généralisation bicatégorique du modèle des espaces de finitude introduit par Ehrhard où nous introduisons une orthogonalité sur la bicatégorie des espèces nous permettant d'obtenir une bicatégorie où les interactions entre programmes et environnements sont finies. Toute la structure de logique linéaire du modèle des espèces peut alors être transposée dans cette nouvelle bicatégorie. Nous considérons ensuite la catégorification de la notion de stabilité des fonctions stables à la Berry vers les foncteurs stables. Nous combinons les espèces de structure avec la stabilité grâce à une orthogonalité sur les sous-groupes d'endomorphismes pour chaque objet d'un groupoïde. Cette orthogonalité peut aussi être traduite en une orthogonalité sur la catégorie de préfaiscaux d'un groupoïde nous permettant de restreindre les foncteurs analytiques associés aux espèces à des foncteurs stables et nous montrons qu'ils forment une bicatégorie cartésienne fermée. Nous étudions dernièrement la catégorification du modèle de Scott de la logique linéaire et son lien avec le modèle des espèces. Nous commençons par montrer que la bicatégorie des profoncteurs équipée de la pseudo-comonade des coproduits finis est un modèle de la logique linéaire catégorifiant le modèle de Scott. Nous introduisons ensuite une orthogonalité entre la bicatégorie de Scott obtenue et la bicatégorie des espèces et obtenons une nouvelle bicatégorie constituant une première étape afin de relier la substitution linéaire et non-linéaire dans ce contexte.