Ce document présente différents outils pour représenter et manipuler des ensembles infinis de n-uplets d'arbres appelés langages de n-uplets d'arbres. Nous avons choisi la programmation logique comme formalisme pour décrire les langages de n-uplets d'arbre (c.à.d. les relations) et les techniques de transformations de programmes pour calculer les opérations sur ceux-ci. Dans un premier temps on étudie une classe de relations closes par la plupart des opérations ensemblistes, la classe des relations pseudo-régulières. Grâce à un lien entre programmes logiques et systèmes de réécriture, nous définissons des classes de systèmes de réécriture conditionnelle dont la clôture transitive est une relation pseudo-régulière. On applique ce résultat pour donner une classe décidable de formules du premier ordre basées sur le prédicat de joignabilité où R est un système de réécriture conditionnel pseudo-régulier. Ensuite on étend ce résultat au second ordre, les variables du second ordre étant interprétées comme des relations. A partir d'un algorithme général original décidant de la satisfiabilité de formules du second ordre sous certaines conditions, nous représentons une instance des variables du second ordre en système de réécriture conditionnel. On montre que ce travail peut permettre la synthèse automatique de programme. Dans un dernier temps, nous utilisons des sur-approximations pour des tests d'inconsistances. A cet effet, nous utilisons une classe de programmes logiques non réguliers dont le test du vide est décidable pour effectuer la sur-approximation. Nous appliquons finalement cette méthode à la vérification de protocoles cryptographiques.

Longtemps méprisé par la littérature générale en raison de son origine populaire, le conte a connu ces trente dernières années un regain d'intérêt général, autant de la part des milieux de la critique et de la recherche que du grand public. Cette attention nouvelle pour un genre qui a été l'apanage de la culture enfantine depuis le succès des Contes de Perrault témoigne de la capacité du conte à s'adapter à toutes les époques. La réécriture des contes que nous nous proposons d'étudier dans ce mémoire traduit un tournant dans l'évolution de ce genre, car ce phénomène florissant est relativement récent dans la littérature de jeunesse. Dans une approche à la fois historique, littéraire et ethnocritique, ce travail vise à étudier, à partir d'un corpus de livres pour enfants, les modes de détournement des contes classiques dans la littérature de jeunesse afin de savoir si la réécriture participe d'un renouvellement du genre. Le premier chapitre retrace l'évolution historique du conte depuis la tradition populaire orale jusqu'à la littérature et sa catégorisation comme genre exclusivement destiné aux enfants, montrant ainsi les liens qui existent entre le conte et la littérature de jeunesse. Après avoir esquissé un panorama des modes de détournement présents dans les récits du corpus, le second chapitre rappelle les principales théories sur la réécriture en littérature. Il se concentre ensuite sur l'analyse des contes détournés à partir des principales composantes du conte merveilleux (espace-temps, personnages et structure). Il s'avère alors que la réécriture conduit à un bouleversement de la forme, des motifs et de la fonction des contes d'origine, puisque sa visée est essentiellement divertissante et ludique. Le dernier chapitre, à teneur plus ethnocritique, se consacre entièrement à l'étude du Petit Chaperon rouge, en montrant la fonction initiatique qu'il possède dans la littérature orale et en expliquant la signification symbolique incarnée par la figure du loup dans l'imaginaire collectif traditionnel. À la lumière des analyses du corpus, il apparaît que la plupart des réécritures de ce conte provoquent son appauvrissement ou tout du moins son altération, dans la mesure où le loup n'est plus générateur d'angoisse pour les lecteurs. En définitive, la réécriture participe à la fois de la redéfinition et du renouvellement du conte, car d'une part elle relève d'un genre distinct dans la mesure où elle rompt avec les valeurs ainsi que le rôle culturel et social que le conte joue toujours dans notre société, et d'autre part elle se situe dans la continuité de son évolution perpétuelle à travers les époques. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Conte, Réécriture, Littérature de jeunesse, Détournement, Petit chaperon rouge, Loup, Charles Perrault.

La richesse de l’anthologie Sette libri di Satire (1560) tient au défi que l’éditeur vénitien Francesco Sansovino relève avec succès à un moment où la Contre-Réforme bat son plein : élaborer une codification en langue vulgaire du genre satirique en rupture avec le genre tel que les auteurs sélectionnés - ou exclus - l’ont pratiqué ou sont censés l’illustrer. L’éditeur oppose le pouvoir de la règle au pouvoir de l’écriture au point de laisser apparaître une triple phase de l’évolution du genre : l’inventio reviendrait à Horace, l’écriture à l’Arioste et la réécriture à Sansovino. L’ensemble de la recherche partagée entre théorie et pratique, vise à interroger cette bipolarité comme une forme de coincidentia oppositorum dans la dialectique que la règle et l’écriture mettent en jeu, autrement dit dans la capacité qu’elles manifestent à « se récuser » et « se fondre l’une l’autre », sur le versant latin et vulgaire. Dans cette optique, loin d’être un exemple de « muséification » des auteurs et des textes, l’anthologie se présente comme la création d’un ‘Hermès bifront’ qui met à son tour le lecteur au défi d’en appréhender les subtilités. / The anthology Sette libri di Satire (1560) is so rich due to the challenge that the Venetian publisher Francesco Sansovino successfully took up at a time when the Counter-Reformation was in full swing. It consisted in elaborating in common language the codification of the literary genre of satire as it broke away from that genre as the authors selected for, or excluded from, the anthology, practised satire or were supposed to exemplify it. To the sway of the rule the anthologist opposes the power of writing, revealing three distinct phases in the development of the genre: the inventio as ascribed to Horace, writing, to Ariosto and re-writing to Sansovino.The research in its entirety, divided as it is between theory and practice, aims to question such bi-polarity as a form of coincidentia oppositorum in the dialectics brought into play by rule and writing, in other words in their ability to reject each other or blend in with each other, within Latin and common language. From this perspective, far from being an example of the transformation of authors and texts into museum pieces, the anthology is presented as the creation of a ‘bi-frontal Hermes’, in turn challenging the reader to grasp its subtleties.

No description available.

Durant ces dernières décennies, nous avons assisté à une automatisation massive de la société selon toutes ses sphères. Malheureusement, cette révolution technologique n’a pas eu que des bienfaits. En effet, une nouvelle génération de criminels en a profité, afin d’occasionner davantage d’activités illégales. De ce fait, afin de protéger les systèmes informatiques, il est devenu plus que primordial de définir rigoureusement des politiques de sécurité ainsi que de mettre en oeuvre des mécanismes efficaces capables de les appliquer. L’objectif majeur d’un mécanisme de sécurité consiste souvent à contrôler des logiciels, afin de les contraindre à “bien” se comporter. Cependant, la plupart des mécanismes de sécurité procèdent par des méthodes ad hoc qui sont loin d’être efficaces. En outre, ils sont peu fiables, puisqu’il n’y a aucune preuve sur leur capacité à faire respecter les politiques de sécurité. De là apparaît la nécessité de concevoir des mécanismes de sécurité alternatifs qui résolvent le problème de l’application de la sécurité d’une manière formelle, correcte et précise. Dans ce contexte, notre thèse cible principalement la caractérisation formelle de l’application effective des politiques de sécurité via des mécanismes basés sur la réécriture de programmes. On entend par application effective, le fait d’éliminer tous les “mauvais” comportements d’un programme, tout en conservant tous les “bons” comportements qu’il engendre, et ce, sans compromettre la sémantique du programme à sécuriser. Nous avons opté pour la réécriture de programmes, vu sa grande puissance par rapport aux autres mécanismes de sécurité qui sont soit laxistes soit très restrictifs. Les principaux résultats qui ont été réalisés, afin d’atteindre les objectifs ciblés par cette thèse sont les suivants : – Caractérisation formelle de l’application des propriétés de sûreté par la réécriture de programmes. Il s’agit d’appliquer les propriétés de sûreté qui constituent la classe de propriétés de sécurité la plus communément appliquée par les mécanismes de sécurité. – Caractérisation formelle de l’application de n’importe quelle propriété de sécurité par la réécriture de programmes. Cette contribution montre comment la réécriture de programmes permet l’application de politiques de sécurité qu’aucune autre classe de mécanismes de sécurité ne peut appliquer. – Caractérisation alternative de l’application de la sécurité par une approche algébrique. Cette contribution propose un formalisme algébrique afin de réduire l’écart entre la spécification et l’implantation des mécanismes de sécurité basés-réécriture. / During the last decades, we have witnessed a massive automation of the society at all levels. Unfortunately, this technological revolution came with its burden of disadvantages. Indeed, a new generation of criminals emerged and is benefitting from continuous progress of information technologies to cause more illegal activities. Thus, to protect computer systems, it has become very crucial to rigorously define security policies and provide the effective mechanisms required to enforce them. Usually, the main objective of a security mechanism is to control the executions of a software and ensure that it will never violate the enforced security policy. However, the majority of security mechanisms are based on ad hoc methods and thus, are not effective. In addition, they are unreliable, since there is no evidence on their ability to enforce security policies. Therefore, there is a need to develop novel security mechanisms that allow enforcing security policies in a formal, correct, and accurate way. In this context, our thesis targets the formal characterization of effective security policies enforcement that is based on programs rewriting. We mean by “effective” enforcement preventing all the “bad” behaviors of a program while keeping all its "good" behaviors. In addition, effective enforcement should not compromise the semantics of controlled programs. We have chosen for rewriting programs, because it has a great power compared to other security mechanisms that are either permissive or too restrictive. Themain contributions of this thesis are the following : – Formal characterization of security enforcement of safety properties through program rewriting. Safety properties represent the main class of properties usually enforced by security mechanisms. – Formal characterization of any security property using program rewriting. This contribution shows how program rewriting allows the enforcement of security policies that no other class of security mechanisms can enforce. – Algebraic approach as an alternative formal characterization of program rewriting based security enforcement. In this contribution, we investigate an algebraic formal model in order to reduce the gap between the specification and the implementation of program rewriting based security mechansisms.

Cette thèse concerne la combinaison du lambda-calcul et de la réécriture, dont nous étudions principalement deux propriétés : la confluence et la normalisation forte. Nous commençons par étudier sous quelles conditions la combinaison d'une relation de réécriture conditionnelle confluente au lambda-calcul donne une relation de réécriture confluente. Ensuite nous nous intéressons aux preuves de normalisation forte de lambda-calculs typés utilisant la technique de réductibilité. Notre contribution la plus importante est une comparaison de diverses variantes de cette technique, utilisant comme outil de comparaison la manière dont ces variantes s'étendent à la réécriture et dont elles prennent en compte les types unions et les types existentiels implicites. Enfin, nous présentons un critère, basé sur un système de types contraints, pour la normalisation forte de la réécriture conditionnelle combinée au lambda-calcul. Notre approche étend des critères de terminaison existants qui utilisent des annotations de taille. C'est à notre connaissance le premier critère de terminaison pour la réécriture conditionnelle avec membres droits d'ordre supérieur qui prenne en compte, dans l'argument de terminaison, de l'information issue de la satisfaction des conditions des règles de réécriture / This thesis is about the combination of lambda-calculus with rewriting. We mainly study two properties: confluence and strong normalization. We begin by studying under which conditions the combination of a confluent conditional rewrite relation to the lambda-calculus leads to a confluent relation. Next, we study strong normalization proofs of typed lambda-calculi that use the reducibility technique. Our main contribution is a comparison of variants of this technique, with respect to how they extend to rewriting and how they handle union and implicit existential types. Finally, we present a termination criterion for the combination of conditional rewriting and lambda-calculus based on a constrained type system. Our approach, which extends known criteria that use sized types, is to our knowledge the first termination criterion for conditional rewriting with higher-order right-hand sides that takes into account in the termination argument some information generated by the satisfaction of the conditions of the rewrite rules

Nous avons dans cette thèse cherché à définir un formalisme simple pour pouvoir modéliser des systèmes où se combinent des phénomènes non-déterministes et des comportements aléatoires. Nous avons choisi d'étendre le formalisme de la réécriture pour lui permettre d'exprimer des phénomènes probabilistes, puis nous avons étudié la terminaison en temps moyen fini de ce modèle. Nous avons également présenté une notion de stratégie pour contrôler l'application des règles de réécriture probabilistes et nous présentons des critères généraux permettant d'identifier des classes de stratégies sous lesquelles les systèmes de réécriture probabilistes terminent en temps moyen fini. Afin de mettre en valeur notre formalisme et les méthodes de preuve de terminaison en temps moyen fini, nous avons modélisé un réseau de stations WIFI et nous montrons que toutes les stations parviennent à émettre leurs messages dans un temps moyen fini.

Les travaux décrits dans ce document ont pour objectif le développement de procédures de décision (et de résolution) pour la vérification. La logique considérée est la logique du premier ordre avec égalité. Cette logique est évidemment indécidable en général, mais l'étude de fragments intéressants pour la vérification peut conduire à des outils automatiques de type "presse-bouton". La notion d'égalité est particulièrement intéressante pour programmer, par orientation des égalités, c'est-à-dire par réécriture, ou pour prouver, grâce au principe de remplacement d'égal par égal. Dans une modélisation en logique du premier ordre avec égalité, on est très facilement amené à utiliser simultanément plusieurs théories différentes pour représenter par exemple les fonctions et la mémoire d'un programme ainsi que les opérations arithmétiques effectuées par le programme. On se retrouve ainsi naturellement face à un problème exprimé dans un mélange de théories, qu'il est souhaitable de résoudre de façon modulaire en réutilisant les procédures de décision connus pour les théories composant le mélange. Cette problématique est au coeur de mes travaux. L'originalité de mon approche consiste à développer des méthodes de combinaison pour les procédures de décision utilisées dans le domaine de la vérification. Toutes les procédures de décision obtenues ont été évidemment élaborées en suivant une démarche de conception sûre, qui s'appuie sur une description à base de systèmes d'inférence pour faciliter leurs preuves.

Partant du sonnet " À une passante " de Baudelaire pour aboutir aux écrits de Breton en parcourant un florilège de textes traitant de la première rencontre, nous avons exploré dans un premier temps les spécificités de la scène poétique relativement à la scène romanesque étudiée par Jean Rousset. Dans un second temps, nous avons cherché à saisir les nouvelles caractéristiques du scénario moderne par rapport aux configurations classique et romantique. En adressant à l'inconnue croisée dans une rue de Paris le poème qu'elle a suscité l'instant d'un coup d'œil fugitif, Baudelaire crée un poncif amoureux nouveau. Dans ce sonnet, le cadre spatio-temporel, les acteurs, la rencontre et l'amour portent l'empreinte de la modernité jusqu'à en devenir l'emblème. D'autres poètes reprendront sur le mode de l'imitation ou de la variation le modèle baudelairien, et notamment la figure de la passante. Le poème de la première rencontre devient alors le lieu de la célébration d'une nouvelle figure féminine mais surtout d'une nouvelle lyrique qui n'est rien de moins qu'une érotique de la distance séparatrice. Chaque poème nous montre à sa façon que l'unique scène signifiante est celle du désir (qui déchire le poète et son lecteur) et que l'écriture d'une rencontre sans issue est l'ultime échappatoire contre l'absence.

Cette thèse propose plusieurs contributions sur le thème de la détection d'implications textuelles (DIT). La DIT est la capacité humaine, étant donné deux textes, à pouvoir dire si le sens du second texte peut être déduit à partir de celui du premier. Une des contributions apportée au domaine est un système de DIT hybride prenant les analyses d'un analyseur syntaxique stochastique existant afin de les étiqueter avec des rôles sémantiques, puis transformant les structures obtenues en formules logiques grâce à des règles de réécriture pour tester finalement l'implication à l'aide d'outils de preuve. L'autre contribution de cette thèse est la génération de suites de tests finement annotés avec une distribution uniforme des phénomènes couplée avec une nouvelle méthode d'évaluation des systèmes utilisant les techniques de fouille d'erreurs développées par la communauté de l'analyse syntaxique permettant une meilleure identification des limites des systèmes. Pour cela nous créons un ensemble de formules sémantiques puis nous générons les réalisations syntaxiques annotées correspondantes à l'aide d'un système de génération existant. Nous testons ensuite s'il y a implication ou non entre chaque couple de réalisations syntaxiques possible. Enfin nous sélectionnons un sous-ensemble de cet ensemble de problèmes d'une taille donnée et satisfaisant un certain nombre de contraintes à l'aide d'un algorithme que nous avons développé. / This thesis presents several contributions on the theme of recognising textual entailment (RTE). The RTE is the human capacity, given two texts, to determine whether the meaning of the second text could be deduced from the meaning of the first or not. One of the contributions made to the field is a hybrid system of RTE taking analysis of an existing stochastic parser to label them with semantics roles, then turning obtained structures in logical formulas using rewrite rules to finally test the entailment using proof tools. Another contribution of this thesis is the generation of finely annotated tests suites with a uniform distribution of phenomena coupled with a new methodology of systems evaluation using error minning techniques developed by the community of parsing allowing better identification of systems limitations. For this, we create a set of formulas, then we generate annotated syntactics realisations corresponding by using an existing generation system. Then, we test whether or not there is an entailment between each pair of possible syntactics realisations. Finally, we select a subset of this set of problems of a given size and a satisfactory a certain number of constraints using an algorithm that we developed