De la construction de preuves à la programmation parallèle en logique linéaire

This thesis aims at studying the construction of linear logic proofs and at using it as a paradigm for parallel programming. We show that inference permutability plays a crucial role in the normalization of proofs in linear logic. This method will then help us to choose a suitable fragment of intuitionistic linear logic for developing a process calculus where logical formulas are interpreted as processes and proofs as interactions between the processes.Cette thèse se propose d'étudier la construction de preuves en logique linéaire et sur la base de cette étude, de l'utiliser ensuite comme paradigme de calcul pour la programmation parallèle.Dans le calcul des séquents linéaire, nous montrons que la propriété de permutabilité d'inférences joue un rôle essentiel dans la normalisation des preuves en vue de leur construction automatique. Cette normalisation est déterminée par deux facteurs: le fragment logique dans lequel nous nous plaçons et le sens de construction des preuves envisagé. Nous mettons ainsi à jour une dualité entre principes de construction des preuves en chaînage avant et principes de construction des preuves en chaînage arrière à partir de laquelle nous proposons une méthode pour normaliser les preuves et élaborer des stratégies de construction dans un fragment donné de la logique linéaire. Appliquée de façon systématique dans la logique linéaire toute entière, elle nous permet d'y proposer une stratégie originale de construction des preuves en chaînage avant.Cette méthode va ensuite nous aider à choisir un fragment approprié de la logique linéaire intuitionniste pour y élaborer un calcul deprocessus asynchrone, CPL (Concurrent Programming Logic), basé sur la construction de preuves. Les formules y sont interprétées comme desprocessus et les preuves, avec certaines restrictions, comme des réductions de processus. Nous proposons une sémantique opérationnelle sous forme d'une relation de transition qui découle de cette interprétation.Pour exprimer la capacité d'interaction des processus avec le monde extérieur, nous proposons une sémantique dénotationnelle, issue de la sémantique des phases de la logique linéaire, qui repose sur les notions de co-processus et d'interface. Un co-processus est un testeur qui caractérise un aspect de l'interaction possible du processus avec l'extérieur. Il est représenté par une formule qui vérifie une certaine forme decomplémentarité avec la formule représentant le processus. Une interface est un ensemble de co-processus caractérisant de manière globale la capacité d'interaction d'un processus avec l'extérieur. Utilisant le cadre déductif, nous construisons un calcul sur les interfaces qui s'articule autour des concepts de réduction et de relativisation d'une interface.La notion de communication synchrone est captée par une simple restriction sur la forme des preuves dans le système déductif de CPL. Cetterestriction permet de définir un calcul synchrone, SCPL qui englobe notamment le pi-calcul de Milner.En tant que modèle logique du parallélisme, CPL peut être un outil d'analyse dans le domaine et peut servir de base à de nouvelles propositions de langages de programmation parallèle. On peut même d'emblée concevoir CPL comme un langage de programmation logique.Enfin, il peut constituer un cadre commun pour l'étude sémantique de programmes écrits dans des langages les plus divers