Cette thèse présente la logique tensorielle, une version primitive de la logique linéaire où la négation involutive est remplacée par une négation tensorielle. Pour illustrer ce point de vue, nous reformulons les espaces cohérents et les espaces de finitude comme deux modèles de logique linéaire obtenus à partir d'un même modèle de logique tensorielle dont on fait varier la négation. La sémantique de la logique tensorielle est pour nous avant tout catégorique, construite autour des notions de catégorie de dialogue et de modalité de ressource. Nous en donnons un modèle inspiré des jeux de Conway où tous les connecteurs, en particulier les modalités de ressource, sont interprétées de manière non dégénérée. Afin de construire ces modalités de ressource de façon plus automatique, nous développons un cadre pour le calcul des algèbres libres d'une T-théorie enrichie. Cette construction, basée sur la notion d'équipement en distributeurs, repose sur deux propriétés : l'une de nature combinatoire, l'opéradicité; l'autre de nature algébrique, la complétude algébrique. Nous présentons ensuite un modèle de jeux équipé d'une trace et d'une notion de multiparenthésage. Le contrôle obtenu par le multiparenthésage est alors vu comme une gestion des ressources. Nous utilisons ce modèle pour interpréter une langage avec références d'ordre supérieur. Nous nous tournons enfin vers des sémantiques de plus bas niveau. Dans un premier temps, nous étudions la structure multicatégorique induite par une catégorie de dialogue. Cela nous amène à définir les multicatégories de contrôle. Dans un second temps, nous formalisons en Coq une propriété de sûreté par le typage d'un compilateur vers un langage assembleur. Cette formalisation repose sur la définition d'une sémantique relationnelle des états de la mémoire dont la structure est inspirée des catégories de dialogue.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00339149 |
| Date | 03 December 2008 |
| Creators | Tabareau, Nicolas |
| Publisher | Université Paris-Diderot - Paris VII |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0019 seconds