Selon le Larousse, un programme informatique est un "ensemble d'instructions et de données représentant un algorithme et susceptible d'être exécuté par un ordinateur." Une forte adéquation entre instructions et données est donc nécessaire afin d'éviter tout dysfonctionnement d'un programme. Nous nous sommes ainsi intéressés ces dernières années aux analyses statiques, réalisées avant l'exécution du programme, permettant de garantir que la manipulation des données se passera correctement. Nous illustrerons nos recherches sur ce thème en considérant trois grandes familles de données: les arbres non ordonnés, les arbres ordonnés (dont XML), et les programmes eux-mêmes en tant que données. Dans chacun de ces domaines, nous avons conçu des analyses statiques, sous forme de système de types ou de bisimulations, adaptés à plusieurs problématiques telles que la manipulation de messages dans un système à composants, les langages bidirectionnels, la manipulation de XML ou les calculs de processus d'ordre supérieur avec passivation.

Les comportements des processus concurrents peuvent être exprimés en utilisant des calculs de processus, des langages formels simples qui permettent de démontrer des résultats mathématiques précis sur les interactions entre processus. Un exemple très simple est CCS, un autre exemple est le pi-calcul, plus expressif grâce à un mécanisme de communication de canaux. Dans ce dernier, on peut instaurer un système de types (pour raffiner l'analyse aux environnements plus contraints) et encoder le lambda-calcul (qui représente les calculs séquentiels).Certains de ces calculs, comme CCS ou des variantes du pi-calcul comme les calculs de fusions, ont une certaine propriété de symétrie. On utilise dans un premier temps cette symétrie comme un outil, pour prouver que deux encodages du lambda-calcul dans le pi-calcul sont en fait équivalents.Cette preuve nécessitant un système de types et une forme de symétrie, on se pose la question de l'existence d'un système de types pour les autres calculs symétriques, notamment les calculs de fusion, à laquelle on répond par la négative avec un théorème d'impossibilité.En analysant ce théorème, on découvre un contrainte fondamentale de ces calculs qui empêche l'utilisation des types, à savoir la présence d'une notion de relation d'équivalence entre les canaux de communication. Le relâchement de cette contrainte pour obtenir une relation de pré-ordre engendre un calcul intéressant qui recouvre des notions importantes du pi-calcul, absentes dans les calculs de fusion : les types et les noms privés. La première partie de la thèse se concentre sur l'étude de ce calcul.La deuxième partie de la thèse se concentre sur la bisimulation, une méthode pour établir l'équivalence de deux agents dans des langages d'ordre supérieur, par exemple le pi-calcul ou le lambda-calcul. Une amélioration de cette méthode est la théorie des techniques modulo, très puissante, mais qui malheureusement s'applique uniquement aux systèmes de premier ordre, comme les automates ou CCS.Cette thèse s'applique alors à décrire les langages d'ordre supérieur en tant que systèmes du premier ordre. On récupère ainsi la théorie générale des techniques modulo pour ces langages, en prouvant correctes la correspondance induite et les techniques spécifiques à chaque langage. On détaille les tenants et aboutissants de cette approche, pour fournir les outils nécessaires à son utilisation pour d'autres langages d'ordre supérieur. / The behaviours of concurrent processes can be expressed using process calculi, which are simple formal languages that let us establish precise mathematical results on the behaviours and interactions between processes. A very simple example is CCS, another one is the pi-calculus, which is more expressive thanks to a name-passing mechanism. The pi-calculus supports the addition of type systems (to refine the analysis to more subtle environments) and the encoding of the lambda-calculus (which represents sequential computations).Some of these calculi, like CCS or variants of the pi-calculus such as fusion calculi, enjoy a property of symmetry. First, we use this symmetry as a tool to prove that two encodings of the lambda-calculus in the pi-calculus are in fact equivalent.This proof using a type system and a form of symmetry, we wonder if other existing symmetric calculi can support the addition of type systems. We answer negatively to this question with an impossibility theorem.Investigating this theorem leads us to a fundamental constraint of these calculi that forbids types: they induce an equivalence relation on names. Relaxing this constraint to make it a preorder relation yields another calculus that recovers important notions of the pi-calculus, that fusion calculi do not satisfy: the notions of types and of privacy of names. The first part of this thesis focuses on the study of this calculus, a pi-calculus with preorders on names.The second part of this thesis focuses on bisimulation, a proof method for equivalence of agents in higher-order languages, like the pi- or the lambda-calculi. An enhancement of this method is the powerful theory of bisimulations up to, which unfortunately only applies for first-order systems, like automata or CCS.We then proceed to describe higher-order languages as first-order systems. This way, we inherit the general theory of up-to techniques for these languages, by proving correct the translations and up-to techniques that are specific to each language. We give details on the approach, to provide the necessary tools for future applications of this method to other higher-order languages.

Le calcul réparti est de plus en plus utilisé bien qu'il reste très mal maîtrisé. Cette thèse porte sur le Dpi-calcul, une extension simple du pi-calcul dans laquelle tous les processus sont placés dans des localités afin de décrire leur répartition. Dans ce calcul, les processus peuvent communiquer localement et migrer entre localités. À côté des canaux de communication et des localités, on identifie une nouvelle famille d'identifiants, les passeports, permettant un contrôle fin des migrations de processus : un processus doit disposer d'un passeport adéquat pour entrer dans une localité.<br /><br />Afin de structurer le calcul, on met en place un système de types qui associe un type à chaque identifiant pour vérifier qu'un processus n'utilise que les droits qu'il possède. L'ordre de sous-typage sur les types est étendu aux types de passeports suivant les localités d'origine des processus migrant. On démontre que cet ordre admet des bornes inférieures sous certaines conditions. On prouve également que les processus se conformant à cette politique de typage conservent cette propriété au cours de leurs réductions.<br /><br />On étudie aussi l'équivalence observationnelle : quand des processus exhibent-ils des comportements indiscernables pour un observateur ? En présence de passeports, il est indispensable d'imposer à l'observateur d'être loyal, c'est-à-dire d'exiger la possession de passeports pour observer les communications ayant lieu dans les localités correspondantes. Ces contraintes définissent une congruence dite barbue loyale. On développe ensuite un système de transitions étiquetées tel que la bisimilarité loyale engendrée coïncide avec cette congruence barbue loyale.

Depuis 2001 j'ai développé au sein de l'équipe Oasis des travaux de recherche sur la sémantique des applications à base d'objets distribués, appliquant dans le contexte d'un vrai langage, et d'applications de taille réelle, mes recherches précédentes dans le domaine des algèbres de processus. Les différents aspects de ce travail touchent naturellement à la sémantique comportementale, et à la définition de procédures de génération de modèles prenant en compte les différentes facettes de la programmation d'applications distribuées, mais aussi, en amont, à l'analyse statique de code et aux techniques d'abstraction de modèles, et en aval aux outils de vérification de propriétés comportementales. Je montre dans ce mémoire la complexité de ces recherches et la grande variété des techniques requises. Nous avons mis en place une méthode cohérente basée sur un modèle sémantique très flexible, le modèle pNets (parameterized Networks of automata), qui nous offre un bon compromis entre décidabilité, complexité, et utilisabilité. Cette approche nous a permis de définir une sémantique comportementale pour différents aspects des applications à base d'objets ou de composants distribués, mais aussi une notion d'abstraction vers des modèles abstraits finis, permettant d'utiliser des outils de vérification de type " model-checking ". L'ensemble de ces aspects a donné lieu à la réalisation de prototypes, dans la plateforme VerCors, et à des cas d'étude de grande taille.

L'extension supersymétrique du Modèle Standard peut contenir des interactions violant la symétrie dite de R-parité. La présence de tels couplages engendrerait une violation des nombres leptonique et/ou baryonique et modifierait en profondeur la phénoménologie de la supersymétrie auprès des futurs collisionneurs de particules. Nous avons développé des tests des interactions violant la R-parité. D'une part, nous avons étudié des signaux clairs de la production d'un seul partenaire supersymétrique de particule du Modèle Standard, qui implique les couplages violant la R-parité, dans le cadre de la physique aux prochains collisionneurs leptoniques et hadroniques. Les résultats montrent que de fortes sensibilités pourront être obtenues sur les paramètres de brisure douce de la supersymétrie et indiquent la possibilité d'une amélioration d'un à deux ordres de grandeur des limites indirectes actuelles sur les valeurs de plusieurs constantes de couplage violant la R-parité. De plus, il a été vérifié que l'analyse de la production d'un seul superpartenaire offre l'opportunité de reconstruire de façon indépendante du modèle théorique diverse masses de superpartenaires avec une grande précision. D'autre part, nous avons étudié des effets de violation de la symétrie CP aux futurs collisionneurs leptoniques dans la production de paire de fermions de saveurs différentes, ou de leur superpartenaire, permettant de mettre en évidence d'éventuelles phases complexes des constantes de couplage violant la R-parité. Nous avons vu notamment que la production d'un quark top accompagné d'un quark charmé permet de tester la violation de CP dans le secteur hadronique. La conclusion de ces travaux est que les phases complexes de certaines constantes de couplage violant la R-parité pourraient être observées, et plus particulièrement dans un scénario où ces couplages exhiberaient une grande hiérarchie dans l'espace des saveurs

Le document traite du raisonnement sur les processus. Les chapitres principaux sont: - Équivalences comportementales : caractérisation logique, axiomatisation et congruence - Inspections et équivalences intensionnelles - Calculs avec localités

Ce travail est une étude approfondie de la concurrence dans les extensions non-déterministes des réseaux d'interaction de Lafont (langage graphique qui représente, lui, le calcul fonctionnel). Ces extensions sont de trois sortes : les réseaux multirègles, multiports et multifils, et leurs combinaisons donnent ainsi sept types de réseaux. Un premier travail consiste à déterminer une bonne sémantique pour pouvoir comparer ces extensions. On cherche à définir un sémantique opérationnelle structurelle sur les réseaux en se basant sur des technique connues de réécriture des graphes, plus particulièrement celle de " double-pushout with borrowed contexts ". Nous définissons à partir de cette méthode un système d'étiquetage des transitions donné par des règles de dérivations dans le style des langages de processus qui sont le paradigme principal pour étudier les systèmes de calcul concurrents. Nous définissons de plus une sémantique observationnelle sur les réseaux basée sur une notion paramétrique de barbe, qui permet enfin de donner avec précision une notion de traduction entre systèmes. On considère qu'une extension est plus expressive qu'une autre si tout langage de la seconde peut être traduit dans un langage de la première. Ceci nous permet de classer l'ensemble des extensions de manière hiérarchique en trois groupe selon la possibilité de traduire un système de réseau dans un autre. Du plus fort au plus faible : les réseaux contenant des multiports ; ensuite ceux contenant des multifils; enfin les réseaux multirègles. Ceci nous permet de donner un langage universel pour les réseaux dont l'étude donne un point de vue neuf sur les briques fondamentales de la concurrence.

Dans cette thèse, nous étudions les notions de déterminisme et de confluence dans des systèmes concurrents et synchrones. Ces derniers sont des variantes du pi-calcul qui ont été étendues avec une notion de temps. Le premier modèle étudié, le S-pi-calcul, est une extension du modèle SL où la réaction à l'absence d'un signal se fait à la fin de l'instant et où les signaux sont considérés comme des valeurs de première classe. Ce modèle utilise les signaux comme mécanisme de communication de base. Dans le cadre du S-pi-calcul, nous avons cherché à développer une théorie compositionnelle de l'équivalence des programmes basée sur la notion de bisimulation. Ensuite, nous avons conçu un système de types en se basant sur une notion d'usage affine pour les signaux que nous avons introduit. Dans ce système, nous avons montré que tout programme typable est déterministe. Le second modèle, TAPIS, est une autre variante du pi-calcul où les canaux sont utilisés pour la communication. Dans ce cadre, nous avons adapté la théorie des types précedemment introduite pour le S-pi-calcul au cas des canaux et montré que les programmes typables sont confluents. Le système développé dans ce contexte ainsi que la preuve du lemme de préservation du typage ont été formalisés dans Coq.