Logique linéaire, Réduction parallèle, Réseaux de preuves, Pi calcul, Chorégraphies, Calcul des processus, Progression, Confluence, Deadlock Freedom

Dans la première partie de ce manuscrit, nous introduisons la première définition de l'élimination parallèle des coupures pour les réseaux de preuves de la logique linéaire multiplicative-exponentielle (MELL). Inspirée par la méthode de Tait et Martin-Löf basée sur la réduction parallèle dans le lambda-calcul, nous abordons les subtilités et défis posés par le cadre des réseaux de preuves non typés. Nous y parvenons en établissant une notion générale de substitution sur des structures plus générales, appelées prestructures. Cela nous permet de définir inductivement l'élimination parallèle des coupures exponentielles sur les prestructures de MELL, notée ¿e.En utilisant la forte confluence de ¿e, nous fournissons la première preuve de confluence pour l'élimination des coupures dans les réseaux de preuves MELL qui ne repose pas sur le lemme de Newman ou la normalisation forte,même indirectement. Enfin, nous étendons la définition de ¿e pour produire l'élimination parallèle des coupures ¿ de MELL. Le lemme du diamant pour¿ offre une preuve alternative de confluence qui reflète pleinement la preuve de Tait et Martin-Löf pour le lambda-calcul. Dans la seconde partie de ce travail, nous introduisons le nouveau système logique PiL : une extension de la logique linéaire multiplicative et additive du premier ordre avec un connecteur non-commutatif non-associatif (¿) et des quantificateurs nominaux (¿ et son dual ¿). Après avoir montré que l'élimination des coupures pour PiL, nous incorporons le fragment sans récursion du π-calculus dans PiL,prouvant que la sémantique opérationnelle du π-calculus est capturée par l'implication linéaire (¿) dans PiL. Nous caractérisons deadlock-freedom,qui garantit qu'un réseau de processus peut continuer à s'exécuter jusqu'à son terminaison. En outre, nous démontrons qu'une caractérisation de progress découle naturellement dans le cas des processes sans mobilité. Nous définissons une correspondance chorégraphies-comme-preuves entre les choreographies et les dérivations, fournissant le premier théorème de complétude pour les choreographies dans ce fragment du π-calculus. Enfn, nous définissons des réseaux de preuves pour ce système en combinant des techniques utilisées dans les réseaux de conflits et les réseaux d'unification, introduisant ainsi la première syntaxe des réseaux de conflits pour MALL avec quantificateurs du premier ordre. Ça nous permets de fournir des représentants canoniques des arbres de calcul modulo entrelacement dans le même style que les réseaux de preuves sont des représentants canoniques des preuves du calcul des séquents.