Cette thèse étudie les propriétés calculatoires des présentations d'opérades, ou systèmes de réécriture de diagrammes de Penrose, et leurs liens avec divers types de systèmes de réécriture classiques. Grâce à des nouveaux critères pour la terminaison et la confluence, on démontre la conjecture sur la convergence de la présentation L(Z2) des Z/2Z-espaces vectoriels, une théorie équationnelle commutative. On montre que les présentations d'opérades sont des généralisations des systèmes de réécriture de mots et des réseaux de Petri et qu'elles fournissent un calcul de gestion explicite des ressources pour les systèmes de réécriture de termes linéaires à gauche. Enfin, on étudie les obstructions à ce même résultat concernant le lambda-calcul. Des annexes présentent les liens entre les opérades et d'autres structures de l'algèbre universelle, ainsi qu'un calcul de substitutions explicites.

Nous présentons une méthode originale de recherche de preuve par récurrence utilisant la surréduction. Elle a la particularité d'être fondée sur la déduction modulo et d'utiliser la surréduction pour sélectionner à la fois les variables de récurrence et les schémas d'instanciation. Elle donne également la possibilité de traduire directement toute dérivation effectuée avec succès en une preuve dans le calcul des séquents modulo. La correction et la complétude réfutationnelle de la méthode sont démontrées en théorie de la preuve. Nous étendons ensuite cette première approche aux théories de réécriture équationnelles constituées d'un système de réécriture R et d'un ensemble E d'égalités. A partir du moment où le système de réécriture équationnel (R,E) possède de bonnes propriétés de terminaison et de complétude suffisante, et si on suppose également que E préserve les constructeurs, la surréduction au niveau des positions les plus profondes où apparaît un symbole défini s'effectue uniquement à l'aide d'unificateurs qui sont également des substitutions constructeurs. Ceci est particulièrement intéressant dans le cas des théories associatives, ou associatives commutatives, pour lesquelles notre système de recherche de preuve a été raffiné.

Les protocoles de sécurité sont des programmes informatiques qui définissent des règles d'échange entre les points d'un réseau et permettent de sécuriser les communications. Ils sont utilisés par exemple dans les distributeurs de billets, les abonnements aux chaînes de télévision payantes, la téléphonie mobile, le commerce électronique. Leur objectif est de garantir le secret d'une donnée, d'authentifier un des participants, de garantir l'anonymat ou la non-répudiation, etc. Ces programmes sont exécutés sur des réseaux ouverts facilement accessibles (comme internet). Aussi, pour démontrer qu'ils remplissent bien leurs objectifs, il est nécessaire de prendre en compte les attaques dont ils peuvent faire l'objet. L'objet de mon mémoire d'habilitation à diriger des recherches est de montrer que les méthodes formelles peuvent être utilisées avec succès pour entreprendre une analyse fine des protocoles cryptographiques, à travers une palette variée d'outils. Nous présentons des procédures pour déterminer de façon automatique si un protocole est sûr. Nous avons proposés différents algorithmes en fonction des propriétés de sécurité considérées ainsi que des primitives cryptographiques utilisées (chiffrement, signature, hachage, ou exclusif, etc.). D'autre part, nous caractérisons des conditions qui permettent de combiner les résultats précédents et de concevoir les protocoles de façon modulaire. Ces résultats se basent sur des modèles symboliques, très différents de ceux utilisés en cryptographie où la notion de sécurité est basée sur la théorie de la complexité. Cette notion de sécurité est mieux adaptée pour identifier toutes les attaques possibles dans la réalité mais, en contrepartie, les (lourdes) preuves de sécurité sont effectuées à la main et semblent difficilement automatisables. Nous avons identifié des hypothèses cryptographiques qui permettent de relier les approches cryptographiques et symboliques. Il est alors possible d'obtenir des preuves de sécurité à un niveau cryptographique, directement à partir des preuves établies (automatiquement) dans un cadre symbolique.

Les évolutions technologiques ont consacré l'émergence des services web et du stockage des données en ligne, en complément des bases de données traditionnelles. Ces évolutions facilitent l'accès aux données, mais en contrepartie soulèvent de nouvelles problématiques de sécurité. La mise en œuvre de politiques de contrôle d'accès appropriées est une des approches permettant de réduire ces risques. Nous étudions ici les politiques de contrôle d'accès au niveau d'un document XML, politiques que nous modélisons par des vues de sécurité XML (non matérialisées) à l'instar de Fan et al. Ces vues peuvent être représentées facilement par des alignements d'arbres grâce à l'absence d'opérateurs arithmétiques ou de restructuration. Notre objectif est par conséquent d'examiner comment manipuler efficacement ce type de vues, à l'aide des méthodes formelles, et plus particulièrement des techniques de réécriture de requêtes et la théorie des automates d'arbres. Trois directions principales ont orienté nos recherches: nous avons tout d'abord élaboré des algorithmes pour évaluer l'expressivité d'une vue, en fonction des requêtes qui peuvent être exprimées à travers cette vue. Il s'avère que l'on ne peut décider en général si une vue permet d'exprimer une requête particulière, mais cela devient possible lorsque la vue satisfait des hypothèses générales. En second lieu, nous avons considéré les problèmes soulevés par la mises à jour du document à travers une vue. Enfin, nous proposons des solutions pour construire automatiquement un schéma de la vue. En particulier, nous présentons différentes techniques pour représenter de façon approchée l'ensemble des documents au moyen d'une DTD. / The evolution of web technologies and social trends fostered a shift from traditional enterprise databases to web services and online data. While making data more readily available to users, this evolution also raises additional security concerns regarding the privacy of users and more generally the disclosure of sensitive information. The implementation of appropriate access control models is one of the approaches to mitigate the threat. We investigate an access control model based on (non-materialized) XML views, as presented among others by Fan et al. The simplicity of such views, and in particular the absence of arithmetic features and restructuring, facilitates their modelization with tree alignments. Our objective is therefore to investigate how to manipulate efficiently such views, using formal methods, and especially query rewriting and tree automata. Our research follows essentially three directions: we first develop new algorithms to assess the expressivity of views, in terms of determinacy, query rewriting and certain answers. We show that those problems, although undecidable in our most general setting, can be decided under reasonable restrictions. Then we address the problem of handling updates in the security view framework. And last, we investigate the classical issues raised by schemata, focusing on the specific "determinism'' requirements of DTDs and XML Schemata. In particular, we survey some techniques to approximate the set of all possible view documents with a DTD, and we provide new algorithms to check if the content models of a DTD are deterministic.

Cette étude est consacrée aux procédés narratifs du récit de voyage de Nerval, du point de vue de l’intertextualité et de l’autobiographie. Dans la première partie, nous abordons le récit de voyage en général, en centrant l’attention sur le voyage littéraire subjectif et autobiographique : son statut spécifique en tant que genre littéraire, son évolution chronologique, ses formes, son intertextualité et son caractère autobiographique. Dans la deuxième partie, nous étudions la spécificité du récit de voyage de Nerval sur le plan narratif, sur celui de l’intertextualité et sur celui de l’écriture autobiographique, selon les différents types des voyages nervaliens : voyage réaliste (Voyage en Orient, Lorely), voyage excentrique (Les Faux Saulniers), voyage parodique (Les Nuits d’octobre), voyage autobiographique (Promenades et Souvenirs) et voyage intérieur (Aurélia). Enfin, dans la troisième partie, nous analysons la poétique du voyage littéraire de Nerval dans la perspective de la modernité de son écriture, en considérant le mélange des formes, les pratiques intertextuelles (référence, réécriture et recomposition), l’originalité du voyageur fantaisiste, le récit poétique et dialogique et l’écriture réaliste. / This study focuses on the narrative processes of travel story of Nerval, in terms of intertextuality and autobiography. In the first part, we discuss of the travel story in general, with a focus on the subjective and autobiographical literary travel : its special status as literary genre, its chronological develpment, its forms, its intertextuality and its autobiographical nature. In the second part, we study specificity of the travel story of Nerval on the narrative level, that of intertextuality and that of autobiographical writing, according to diffrents types of Nerval’s travels : realistic travel (Voyage en Orient, Lorely), eccentric travel (Les Faux Saulniers), parodic travel (Les Nuits d’octobre), autobiographical travel (Promenades et Souvenirs) and interior travel (Aurélia). Finally, in the third part, we analyse the poetics of travel writing of Nerval in the context of the modernity of his writing, considering the mixture of forms, the intertextual practices (reference, rewriting and reorganzation), the originality of fanciful traveler, the poetic and dialogic stroy and realistic writing.

La littérature gabonaise, forte de son dynamisme, voit davantage d’écrivains faire le choix de décrire les réalités sociales dans une langue française réappropriée. Ce qui consiste pour eux à réinventer le français, à l’image de leur société, et à en faire leur propre langue d’écriture. Notre thèse se propose d’étudier ce phénomène dans le polar gabonais, ce genre en plein essor représenté par Janis Otsiémi, et de démontrer que la créativité du point de vue de la langue reste indissociable de l’engagement et de la conviction de l’écrivain gabonais, et afro-subsaharien par extension. En premier abord, il est question de distinguer la langue d’écriture de l’écriture de la langue. Pour cela, étudier les stratégies d’écriture de l’écrivain, relever les divers gabonismes et africanismes présents dans le roman d’Otsiémi et les fonctions propres à chacune des particularités linguistiques, nous permet de faire état de l’esthétique littéraire et des pratiques langagières gabonaises. En second lieu, l’objectif est pour nous de procéder à une herméneutique de l’oeuvre d’Otsiémi pour dégager grâce à la subversion de l’écriture la poétique subversive de son oeuvre. Pour ce faire, situer le style de l’auteur revient à évaluerl’engagement de l’auteur vis-à-vis de la langue et de l’écriture, à faire face à une écriture hybride résultant du foisonnement des intertextes, et à aborder l’identité à la fois revalorisée et déconstruite par l’auteur, respectant ainsi le principe élémentaire du polar qu’est celui d’écrire le noir. / The Gabonese literature, strong in its dynamism, sees more writers make the choice to describe social realities in a French language reappropriated. What is for them to reinvent the French, in the image of their society, and to make their own language of writing. Our thesis proposes to study this phenomenon in the Gabonese crime novel, this booming genre represented by Janis Otsiemi, and to demonstrate that creativity from the point of view of language remains inseparable fromthe commitment and conviction of the Gabonese writer, and afro-sub-Saharan by extension. At first, it is a question of distinguishing the language of writing from the writing of the language. To do this, to study the writer's writing strategies, to identify the various gabonisms and Africanisms present in Otsiemi's novel and the functions proper to each linguistic peculiarity, allows us to describe literary aesthetics and Gabonese languages practices. In the second place, the objective is for us to proceed with a hermeneutic of the work of Otsiemi to free, thanks to the subversion of writing, the subversive poetics of his work. To do this, situating the author's style amounts to evaluating the author's commitment to language and writing, to coping with a hybrid writing resulting from the proliferation of intertexts, and to approach the identity both revalorized and deconstructed by the author, thus respecting the elementary principle of the crime novel that is to write black.

Ce document décrit mon travail de recherche et programmation en informatique effectué entre 1990 et 2005.<br />Tout ce travail s'inscrit dans le cadre des systèmes de réécriture de termes et des stratégies "appel-par-valeur". Il est à la fois théorique et pratique; la plupart des notions et algorithmes étudiés ont été implémenté dans le logiciel Autowrite.<br /><br />Ce document est une opportunité de présenter tous nos travaux dans ce domaine (publiés ou non) dans un cadre uniforme.<br />Du fait de la non limitation du nombre de pages, cette présentation contient plus de détails et d'exemples qu'on ne peut généralement en donner dans une publication classique.

Ce manuscrit présente les travaux de recherche, d'encadrement et de développement que j'ai effectués au cours des huit dernières années. Ma première motivation a été de rendre utilisables les concepts liés à la notion de réécriture. Pour cela, ma stratégie a consisté à proposer un langage, dénommé Tom, construit comme une extension de langages existants, et non comme un langage à part entière. L'intérêt principal de cette approche, appelée Îlot Formel, est de fournir de nouvelles constructions aux programmeurs sans pour autant changer leur environnement de travail.<br />Cette approche, permettant de combiner différents formalismes est étudiée d'un point de vue formel.<br />Dans un deuxième temps, je me suis intéressé à la confiance que les programmeurs peuvent avoir dans les programmes qu'ils écrivent et dans les outils qu'ils utilisent.<br />Ces travaux m'ont amené à proposer des constructions de haut niveau (filtrage équationnel, anti-termes et stratégies) ainsi qu'à formaliser leur sémantique.<br />Nous présentons également une méthode originale qui permet certifier que le code produit par le compilateur Tom préserve bien la sémantique de ces constructions.

L'algorithme de complétion de Knuth-Bendix permet, dans certains<br />cas, d'utiliser les systèmes de réécriture pour décider le<br />problème du mot dans un monoïde. Le problème du mot est alors<br />réduit a un calcul de forme normale. Cependant, tous les monoïdes<br />décidables ne peuvent pas être résolus de cette façon. Un<br />programme, initie par Squier, vise a caractériser par des<br />invariants algébriques la classe des monoïde décidables par<br />réécriture.<br />L'objectif de cette thèse est d'étendre ce travail a la réécriture<br />de termes.<br />Nous établissons des conditions de finitude homologique pour<br />l'existence de présentations convergentes de type fini par<br />réécriture de termes de théories équationnelles du premier ordre<br />avec une sorte. Une théorie équationnelle est sémantiquement<br />décrite par une théorie algébrique au sens de Lawvere. Nous<br />introduisons l'homologie de ces théories à coefficients dans les<br />bimodules non additifs, comme généralisation de l'homologie de<br />MacLane des anneaux. Cette homologie admet une interprétation en<br />terme d'homologie de Hochschild-Mitchell de la petite catégorie<br />sous-jacente. Nous généralisons les résolutions libres de Squier<br />et Kobayashi, établies en réécriture de mots, à la réécriture de<br />petites catégories. En utilisant ces résolutions, nous montrons<br />qu'une théorie algébrique admettant une présentation convergente<br />de type fini est de type bi-$\mathrm(PF)_(\infty)$. Nous<br />construisons une théorie équationnelle, non unaire, décidable et<br />n'admettant pas de présentation convergente de type fini.

Cette thèse s'inscrit dans l'étude de familles de graphes infinis de présentation finie, de leurs propriétés structurelles, ainsi que des comparaisons entre ces familles. Étant donné un alphabet fini Σ, un graphe infini étiqueté par Σ peut être caractérisé par un ensemble fini de relations binaires (Ra )a∈Σ sur un domaine dénombrable V quelconque. De multiples caractérisations finies de tels ensembles de relations existent, soit de façon explicite grâce à des systèmes de réécriture ou à divers formalismes de la théorie des automates, soit de façon implicite. Après un survol des principaux résultats existants, nous nous intéressons plus particulièrement à trois problèmes. Dans un premier temps, nous définissons trois familles de systèmes de réécriture de termes dont nous démontrons que la rela- tion de dérivation peut être représentée de façon finie. De ces résultats découlent plusieurs questions sur les familles de graphes infinis correspondantes. Dans un se- cond temps, nous étudions deux familles de graphes dont les ensembles de traces forment la famille des langages contextuels, à savoir les graphes rationnels et les graphes linéairement bornés. Nous nous intéressons en particulier au cas des langages contextuels déterministes, ainsi qu'à la comparaison structurelle de ces deux familles. Enfin, d'un point de vue plus proche du domaine de la vérifica- tion, nous proposons un algorithme de calcul des prédécesseurs pour une famille d'automates à pile d'ordre supérieur.