Les données ont toujours été un atout clé pour beaucoup d’industries et d’entreprises ;cependant, ces derniers temps les possesseurs de données jouissent d’un véritable avantage compétitif sur les autres. De nos jours, les compagnies collectent de gros volumes de données et les stockent dans de grandes bases de données multidimensionnelles appelées entrepôts de données. Un entrepôt de données présente les données agrégées sous la forme d’un cube dont les cellules contiennent des faits et des informations contextuelles telles que des dates, des lieux, des informations sur les clients et fournisseurs, etc. Les solutions d’entreposage de données utilisent avec succès OLAP (Traitement Analytique En Ligne – en anglais Online Analytical Processing) afin d’analyser ces grands ensembles de données ;par exemple, les informations des ventes peuvent être agrégées selon le lieu et/ou la dimension temporelle. Les tendances récentes des technologies et du Web posent actuellement de nouveaux défis. Une bonne quantité de l’information disponible sur le Web s’y trouve sous une forme qui se prête au traitement par machine (Web Sémantique) ;les outils de veille économique (en anglais Business Intelligence ou BI) doivent être capables de découvrir et récupérer les informations pertinentes, et les présenter aux utilisateurs afin de les assister dans une bonne analyse de la situation. De nombreux gouvernements et organisations rendent leurs données publiquement accessible, identifiables avec des URI (Unified Resource Identifiers), et les lient à d’autres données. Cette collection de jeux de données interconnectés sur le Web s’appelle Linked Data [1]. Ces jeux de données sont basés sur le modèle RDF (Resource Description Framework) – un format standard pour l’échange de données sur le Web [2]. SPARQL, un protocole et un langage de requêtes pour RDF [4], est utilisé pour interroger et manipuler les jeux de données RDF stockés dans des triplestores SPARQL. SPARQL 1.1 Federated Query [6] définit également une extension pour exécuter des requêtes distribuées sur plusieurs triplestores. Le standard actuel permet donc des requêtes analytiques complexes sur de multiples sources de données, et l’intégration de ces données dans le processus d’analyse devient une nécessité pour les outils de BI. Cependant, en raison de la quantité et de la complexité des données disponibles sur le Web, leur incorporation et leur utilisation ne sont pas toujours évidentes. Par conséquent, une solution OLAP efficace sur des source Web Sémantiques est nécessaire pour améliorer les outils de BI. Cette thèse de doctorat se concentre sur les défis liés à l’optimisation des requêtes analytiques qui utilisent des données provenant de plusieurs triplestores SPARQL. Premièrement, cette thèse propose un framework pour la découverte, l’intégration et l’interrogation analytique des Linked Data – ce type d’OLAP a été nommé OLAP Exploratoire [21]. Ce framework est conçu pour utiliser un schéma multidimensionnel du cube OLAP exprimé dans des vocabulaires RDF, afin de pouvoir interroger des sources de données, extraire et agréger des données, et construire un cube de données. Nous proposons également un processus assisté par ordinateur pour découvrir des sources de données précédemment inconnues et construire un schéma multidimensionnel du cube. Deuxièmement, vu l’inefficacité actuelle des triplestores SPARQL pour l’exécution des requêtes analytiques fédérées, cette thèse propose un ensemble de stratégies pour le traitement de ces requêtes ainsi qu’un module (appelé Cost-based Optimizer for Distributed Aggregate ou CoDA) pour optimiser leur exécution. Troisièmement, afin de surmonter les défis liés aux techniques de traitement des requêtes SPARQL agrégées sur un seul triplestore, nous proposons MARVEL (MAterialized Rdf Views with Entailment and incompLeteness) – une approche qui utilise des techniques de vues matérialisées spécifiques à RDF pour traiter les requêtes agrégées complexes. Notre approche consiste en un algorithme de sélection de vues selon un modèle de coût associé spécifique à RDF, une syntaxe pour la définition des vues et un algorithme pour la réécriture des requêtes SPARQL en utilisant les vues matérialisées RDF. Finalement, nous nous concentrons sur les techniques relatives au support des requêtes analytiques SPARQL sur des données liées situées en de multiples triplestores, qui nous conduisent à d’intéressantes analyses et constatations à grande échelle. En particulier, la technique proposée est capable d’intégrer les schémas divers des endpoints SPARQL, donnant accès aux données via des hiérarchies dans le style d’OLAP pour permettre des analyses uniformes, efficaces et puissantes. Enfin, cette thèse préconise une plus grande attention au traitement des requêtes analytiques au sein des systèmes RDF distribués. / Doctorat en Sciences de l'ingénieur et technologie / info:eu-repo/semantics/nonPublished

Le but de cette thèse est de trouver des modèles de haut niveau dans lesquelles l'auto-modification s'exprime facilement. Une donnée est lisible et modifiable, alors qu'un programme est exécutable. On décrit une machine abstraite où cette dualité est structurellement mise en valeur. D'une part une zone de programmes contient tous les registres exécutables, et d'autre part une zone de données contient les registres lisibles et exécutables. L'auto-modification est permise par le passage d'un registre d'une zone à l'autre. Dans ce cadre, on donne une abstraction de l'exécution de la machine qui extrait seulement les informations d'auto-modification. Logiquement, on essaye de trouver une correspondance de Curry-Howard entre un langage avec auto-modification et un système logique. Dans ce but on construit une extension de lambda-calcul avec termes gelés, c'est à dire des termes qui ne peuvent se réduire. Ces termes sont alors considérés comme des données, et les autres sont les programmes. Notre langage a les propriétés usuelles du lambda-calcul (confluence). D'autre part, on donne un système de types dans lequel un sous ensemble des termes du langage peuvent s'exprimer. Ce système est inspiré de la Logique Linéaire, sans gestion des ressources. On prouve que ce système de types a de bonnes propriétés, comme celle de la réduction du sujet. Finalement, on étend le système avec les continuations et la double négation, dans un style à la Krivine / The goal of my Ph.D. is to finds high level models in which self-modification can be expressed. What is readable and changeable is a data, and a program is executable. We propose an abstract machine where this duality is structurally emphasized. On one hand the program zone beholds registers which can be executed, and on the other hand data zone contains readable and changeable registers. Self-modification is enabled by passing a data register into program zone, or a program register into data zone. In this case, we give an abstraction of executions which only extracts information about self-modifications: execution is cut into paths without self-modification. For the logical part, we tried to find a Curry-Howard correspondence between a language with self-modifications and logical world. For that we built an extension of lambda-calculus with frozen terms, noted <t>, that is, terms which cannot reduce. This terms are considered as data. Other terms are programs. We first prove that this language as expected properties like confluence. On the other hand, we found a type system where a subset of terms of this language can be expressed. Our type system is inspired by Linear Logic, without resources management. We prove that this system has good properties like subject reduction. We finally have extended the system with continuation and double negation. This extension can be expressed in a krivine style, using a machine inspired by krivine machine

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.

Le calcul massivement parallèle a connu durant ces deux dernières décennies un fort développement. Les efforts dans ce domaine ont d'abord surtout été orientés vers les machines, plutôt qu'à la définition de langages adaptés au parallélisme massif. Par la suite, deux principaux modèles de programmation ont émergé : le parallélisme de contrôle et le parallélisme de données. Le premier a connu un vif succès. Dans ce modèle cependant, les applications massivement parallèles s'avèrent difficiles à concevoir et peu fiables, compte tenu du grand nombre de processus envisagés. En revanche, le parallélisme de données paraît aujourd'hui être un bon compromis entre les besoins des utilisateurs et les contraintes imposées par les architectures parallèles. Dans cette thèse, nous nous sommes intéressé à la validation formelle des langages à parallélisme de données. L'idée est de tirer parti de la relative simplicité de ce modèle de programmation pour développer des méthodes semblables à celles déjà éprouvées dans le cadre des langages scalaires classiques. La première partie du travail effectué concerne un langage data-parallèle simple, de type impératif. Nous avons montré qu'il était possible de définir un système de preuve complet pour ce langage, inpiré de la logique de Hoare. L'étude théorique nous a permis en outre de définir une méthodologie pratique de preuve par annotations, semblable à celle utilisée pour les langages scalaires. Nous nous sommes ensuite tourné vers le langage d'équations récurrentes Alpha. Il s'avérait nécessaire de définir pour ce langage un cadre formel de validation, plus riche que le système de transformations existant ne permettant que des preuves par équivalence. Nous avons défini un modèle d'exécution par l'intermédiaire d'une sémantique opérationnelle, et une méthodologie de preuve. Celle-ci utilise des invariants qui sont raffinés à partir d'une traduction du programme dans un langage logique jusqu'à l'obtention de la propriété voulue.

Dans cette thèse, nous proposons un langage formel, le gk-calcul, issu de la famille des algèbres de processus. Ce langage se distingue notamment des langages concurrents habituels par la rupture de la dissymétrie inhérente à la notion d'émetteur et de récepteur traditionnellement considérée. Cette rupture permet alors de voir les interactions entre les éléments du langage comme des phénomènes de collisions, approche bien adaptée aux questions d'auto-organisation qui font l'objet de la première partie de cette thèse.<br /><br />La question qui se pose est celle de la construction concurrente et décentralisée de formes géométriques abstraites (arbres et graphes) ainsi que de phénomènes plus génériques décrits sous forme de transfert d'information dans des systèmes à base de réécriture de graphes, éventuellement hiérarchisés dans l'optique d'une application à la biologie moléculaire. Cette première partie s'accompagne notamment d'une implémentation en Ocaml simulant un algorithme d'auto-assemblage de graphes.<br /><br />Dans un second temps, nous développons un sous-ensemble du langage présenté, en enrichissant une version restreinte aux interactions binaires avec une notion de membrane et d'interactions entre membranes. Ce nouveau langage se montre à même de décrire une biologie moléculaire simplifiée, qualitative, basée sur les interactions entre protéines et membranes. Cette partie de la thèse s'attache alors à montrer la valeur descriptive de ce langage sur quelques exemples et à explorer des définitions pertinentes d'équivalence entre solutions biologiques.