Ce travail s'intéresse à la preuve de propriétés de sûreté sur les programmes. Prouver de telles propriétés revient généralement à démontrer que les configurations critiques ne sont jamais atteintes lors de l'exécution du programme. Pour ces propriétés, nous proposons une technique de vérification semi-automatique qui tente de combiner les avantages du model-checking, interprétation abstraite et preuve interactive. Comme en model-checking, cette technique permet de prouver automatiquement des propriétés de sûreté sur les systèmes finis, ainsi que sur certaines classes de systèmes infinis ayant une présentation finie. En dehors de ces classes et comme en interprétation abstraite, notre technique permet d'approcher le comportement infini d'un système par une sur-approximation sûre. Enfin, lorsque les approximations sont trop grossières, il nous est possible d'intervenir manuellement sur la définition des approximations afin de les raffiner et, si cela est possible, de mener la preuve à son terme. Cette approche est basée sur les systèmes de réécriture qui sont un des outils centraux de la déduction automatique. Nous les utilisons comme formalisme pour représenter les programmes: une configuration de programme est représentée par un terme et les transitions entre configurations par des règles de réécriture. Sur de tels modèles, prouver la sûreté d'un programme revient à faire une analyse d'atteignabilité, c.-à-d. vérifier que les termes représentant les configurations critiques sont inatteignables par réécriture des termes initiaux. L'ensemble des termes atteignables est représenté par un automate d'arbre. La construction de cet automate est effectuée en utilisant un algorithme de complétion spécifique. Pour la définition des approximations, nous avons proposé deux langages spécifiques, l'un calqué sur la structure des automates et l'autre utilisant des équations sur les termes. Ce dernier permet, en particulier, d'estimer la précision des approximations construites par rapport à la réécriture modulo équations. Cette technique a été expérimentée pour la vérification de protocoles cryptographiques ainsi que pour le protoypage rapide d'analyses statiques de programmes Java byte code.

Il était une fois...l'histoire d'une petite fille curieuse qui, en suivant un lapin blanc, découvre un pays merveilleux habité par d'étranges créatures. Cette fillette et cet univers, nous les connaissons, c'est l'Alice au pays des merveilles de Lewis Carroll. Ce conte a fait du chemin depuis sa parution en 1865 et ses pas l'ont mené jusqu'à aujourd'hui dans les mains d'un pionnier de la littérature d'horreur au Québec: Patrick Senécal. Depuis 1994, cet auteur est de plus en plus présent dans le panorama littéraire québécois, mais c'est son quatrième roman, Aliss, publié en 2000, qui retient ici notre attention. Dans ce roman, Senécal réécrit l'Alice au pays des merveilles de Carroll à l'aide d'un travail intertextuel et de réécriture. L'enjeu de ce mémoire est de découvrir de quelle manière s'opère la réécriture transformant le conte de Carroll en un nouveau texte qui propose une version moderne du sujet. Le récit de Senécal s'inscrit dans ce que Gérard Genette appelle l'hypertextualité : toute relation qui unit un texte (hypertexte) à un autre texte (hypotexte) dont il dérive. Dans nos recherches, ce sont les théories et la typologie intertextuelle qui servent de premiers moyens d'investigation. En sollicitant les catégories de la citation, de la référence et de l'allusion, nous sommes en mesure d'identifier et d'étudier les relations qu'entretient le récit de Senécal avec le conte de Carroll, mais également avec d'autres intertextes. Les théories de la réécriture et les concepts de répétition et de variation qui lui sont relatifs nous permettent d'analyser en profondeur les transformations apportées à Alice au pays des merveilles pour devenir Aliss. La réécriture joue notamment sur trois aspects. On assiste d'abord à un changement générique qui fait que l'on passe du merveilleux à une oeuvre se trouvant à la frontière entre le récit fantastique et le récit d'horreur. C'est notamment l'aspect cauchemardesque et fantastique déjà suggéré dans le conte de Carroll qui devient la source du glissement de genre. Pour parler de réécriture, il faut que l'on en reconnaisse obligatoirement le modèle. L'étude de la transposition des épisodes et des personnages d'Aliss, construits en miroir avec leur double carrollien et influencés par le changement générique, est donc nécessaire à la compréhension du phénomène. Finalement, en plus de s'approprier le conte de Carroll, Senécal intègre dans son récit l'auteur d'Alice au pays des merveilles et en fait un horrible personnage. Dans le dernier chapitre, la manière dont Senécal reprend les éléments caractéristiques de la vie de Carroll et de son oeuvre pour construire ce double subversif est étudiée. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Intertextualité, Réécriture, Fantastique, Horreur, Conte, Lewis Carroll, Patrick Senécal, Alice au Pays Des Merveilles, Aliss.

Le conte de fées naît à une époque où l'idéal de l'homme civilisé gagne en popularité. Certains auteurs, issus pour la plupart de la société de cour, puisent des contes dans la tradition orale et en font des adaptations littéraires. Avec son inscription littéraire, le conte merveilleux devient un outil pédagogique. Son contenu est donc adapté de manière à en faire un vecteur du modèle de civilité : il faut apprendre aux enfants à se comporter conformément à cet idéal. Ceci est bon pour les deux sexes. Cependant, l'idéal de la femme civilisée est beaucoup plus prescriptif et restrictif que celui de l'homme civilisé : si l'on peut pardonner à ce dernier, ou même valoriser, son tempérament sanguin, les pulsions féminines sont tout simplement inacceptables. On s'attend de la femme qu'elle soit toujours irréprochable, autant sur le plan de son apparence que de son comportement. L'idéologie patriarcale qui va de pair avec celle de la civilité reproche à la femme toute marque d'initiative ou d'individualité. On veut qu'elle soit passive, soumise, vertueuse et prude. Ainsi, beaucoup de contes de fées s'adressent aux petites filles et leur enseignent les bons et les mauvais comportements. L'idéologie patriarcale véhiculée par le conte de fées a fait l'objet de critiques féministes, particulièrement dans les années 1970. On a reproché au conte de fées d'encourager la passivité féminine à travers une représentation stéréotypée des rôles sexuels. On a aussi condamné la représentation de la femme-objet : l'apparence physique de la femme est centrale dans le conte de fées. Si les héros connaissent le succès grâce à leurs actions, les héroïnes doivent tout à leur beauté. Ces diverses critiques ont ouvert la voie à plusieurs réécritures féministes du conte de fées. Certains écrivains et écrivaines ont créé de nouvelles histoires en empruntant la structure traditionnelle du conte de fées, d'autres ont plutôt choisi de transformer des contes déjà connus. Dans ce mémoire, nous proposons, pour commencer, un survol de l'évolution du conte de fées, de son origine orale à ses subversions littéraires contemporaines, en lien avec certaines transformations sociales. Nous étudierons, par la suite, deux réécritures de contes de fées qui, à notre avis, possèdent un caractère féministe. Il s'agit de « La femme de l'Ogre » de Pierrette Fleutiaux (1984) et de Peau d'âne de Christine Angot (2003). Ces deux récits qui vont à l'encontre du discours patriarcal propre aux contes de fées traditionnels évoquent des idéologies féministes opposées. Plusieurs éléments du texte de Fleutiaux correspondent à l'idéologie du féminisme de la femelléité tandis que le récit d'Angot évoque l'idéologie du courant féministe matérialiste. Nous verrons de quelle manière elles parviennent toutes deux, à travers des écritures du corps qui diffèrent grandement l'une de l'autre, à contrecarrer la représentation du corps féminin objet, perçu selon le regard masculin, qui est caractéristique du conte de fées traditionnel. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Conte de fée, patriarcat, féminisme, subversion, réécriture.

La première partie de ce mémoire consiste en une réécriture en prose, sous forme de roman, de la pièce Antigone de Sophocle. Antigone habite, sous le nom de Marie-Ange Gobeil, une résidence pour personnes âgées, en compagnie d'une aide-ménagère, Geneviève. Le récit commence avec le retour de Hémon, qui emménage dans un immeuble près de chez elle. Réapparaissent ensuite les personnages qui entouraient Antigone dans la tragédie. Ces retours n'ont cependant pas d'importance pour Antigone puisque la réapparition des siens ne change rien à la mort de son frère. Le retour d'Ismène, toutefois, a cela de particulier qu'il ramène non le passé mais le présent; ainsi la sœur d'Antigone lui apparaît toujours jeune, croyant que la prise de Thèbes et la mort de leur frère se sont produits le jour précédent. Le roi Créon réapparaît pour justifier sa rancœur et déployer contre Antigone sa hargne. Prise entre une souffrance renouvelée et la mort passée de son frère, Antigone ne choisit ni l'une ni l'autre. La seconde partie prend la forme d'un essai tenant compte de l'apport du travail créateur dans une réflexion sur l'écriture. Ainsi, en premier lieu, j'aimerais proposer une réflexion méthodologique sur ce que peut représenter un essai réflexif en lien avec une pratique de création, de façon à ce que l'essai puisse éclairer la nature même de sa démarche réflexive. En second lieu, j'aimerais envisager une interrogation plus grande qui remet en question l'indépendance, en création littéraire, de la poièsis et de la mimésis, c'est-à-dire des activités de fabrication et d'imitation. En rapport avec ces deux théories, je développerai ce que mon propre travail m'a appris sur l'imitation en fonction de la réécriture. Ce travail me permet d'avancer trois thèses : a) l'écriture est essentiellement une suite de choix, b) en écriture, l'imitation porte sur un modèle absent et intérieur et c) l'écrivain est toujours seul avec l'écriture. Ces trois thèses seront au centre d'un travail réflexif qui interrogera la théorie littéraire sur les notions d'imitation, de réécriture et de solitude. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Antigone, Hémon, Tragédie, Réécriture, Théorie de la création littéraire, Imitation, Mimésis, Solitude.

Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.<br />La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.<br />La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.<br />La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.

L'exode rural des Maori suivant la seconde guerre mondiale a bouleversé le paysage socioculturel néo-zélandais. Cette thèse explore une de ses conséquences directes : l'émergence de gangs maori comme tentative de re-territorialisation de l'espace environnant dans une logique de différentiation par rapport à l'ordre établi. La rupture avec la ville européenne et les traditions ancestrales maori s'imposait. Le gang dit " maori " ne pouvait, et ne peut plus, dès lors être pensé dans le prolongement du tribalisme et du bellicisme maori pré-colonial, analyse figeant le Maori dans des considérations essentialistes. Cette thèse présente le gang maori comme un produit historique contingent et vise, sans cautionner l'approche essentialiste, à déterminer les effets de cette posture analytique sur les pratiques quotidiennes du membre de gang, ainsi que ses rapports au public.Les gangs, qui souhaitaient inventer un espace qui leur était propre, finirent par admettre leur héritage maori, si bien que les membres allaient non seulement réécrire l'histoire de leur organisation en lui trouvant d'autres origines, mais aussi celle du passé maori pré-colonial en y introduisant des éléments propres au gang de rue contemporain

Ayant recours aux théories de l’intertextualité et de la citation telles que développées par Genette, Compagnon et Morawski, ce mémoire met en relation deux corpus distincts mais complémentaires : les principaux essais d’Hubert Aquin, de Gaston Miron et des collaborateurs de la revue Parti pris sont analysés comme réécriture des textes (ou réélaboration des idées) d’Aimé Césaire, de Frantz Fanon et d’Albert Memmi, figures dominantes du discours de la décolonisation francophone. L’approche adoptée vise à mettre en lumière les bases sur lesquelles les intellectuels québécois tâchèrent de justifier leur réutilisation du discours de la décolonisation. Elle permet aussi d’observer dans quelle mesure ce discours orienta la réflexion entourant la redéfinition du nationalisme au Québec, en plus de faciliter sa diffusion. Articulé autour de trois grands axes – l’identité culturelle, les conflits linguistiques ainsi que le rôle de la littérature et de l’écrivain dans le combat pour l’émancipation nationale –, ce mémoire démontre que l'établissement d'un tel partenariat symbolique a été d'un grand apport quant à l'appartenance du Québec à la francophonie. / Refering to the theories of Genette, Compagnon and Morawski's on quotation and intertextuality, this thesis compares two distinct, yet complementary, body of works: the major essays written by Hubert Aquin, Gaston Miron and the young intellectuals who collaborated to Parti Pris are analyzed as rewriting (or rethinking) of the works of Aimé Césaire, Frantz Fanon and Albert Memmi, figureheads of the francophone decolonization movement. The main objective of this study is to investigate the bases on which Québécois intellectuals attempted to justify their recuperation of the discourse of decolonization, and how this discourse shaped their reflection towards redefining Québec nationalism, as well as promoting its diffusion. Articulated around three principal axes – cultural identity, language conflicts and the role of literature and the writer in the struggle for national emancipation –, this thesis shows that the creation of such a symbolic partnership has enabled Québec to join the community of francophone nations.

Les systèmes informatiques jouent un rôle essentiel dans la vie actuelle, et leurs erreurs peuvent avoir des conséquences dramatiques. Il existe des méthodes formelles permettant d'assurer qu'un système informatique est fiable. La méthode formelle utilisée dans cette thèse est appelée complétion d'automates d'arbres et permet d'analyser les systèmes à nombre d'états infini. Dans cette représentation, les états du système sont représentés par des termes et les ensembles d'états par des automates d'arbres. L'ensemble des comportements possibles d'un système est calculé grâce à l'application successive d'un système de réécriture modélisant le comportement du système vérifié. On garantit la fiabilité d'un système en vérifiant qu'un comportement interdit n'est pas présent dans l'ensemble des états accessibles. Mais cet ensemble n'est pas toujours calculable, et nous devons alors calculer une sur-approximation calculable de cet ensemble. Mais cette approximation peut s'avérer trop grossière et reconnaître de faux contre-exemples. La première contribution de cette thèse consiste alors à caractériser, par des formules logiques et de manière automatique, ce qu'est une "bonne" sur-approximation : une approximation représentant un sur-ensemble des configurations accessibles, et qui soit suffisamment précise pour ne pas reconnaître de faux contre-exemples. Résoudre ces formules conduit alors automatiquement à une sur-approximation concluante si elle existe, sans avoir recours à aucun paramétrage manuel. Le second problème de la complétion d'automates d'arbres est le passage à l'échelle, autrement dit le temps de calcul parfois élevé du calcul de complétion quand on s'attaque à des problèmes de la vie courante. Dans la vérification de programmes Java utilisant la complétion d'automates d'arbres, cette explosion peut être due à l'utilisation d'entiers de Peano. L'idée de notre seconde contribution est alors d'évaluer directement le résultat d'une opération arithmétique. D'une façon plus générale, il s'agit d'intégrer les éléments d'un domaine infini dans un automate d'arbres. En s'inspirant de méthodes issues de l'interprétation abstraite, cette thèse intègre des treillis abstraits dans les automates d'arbres, constituant alors un nouveau type d'automates. Les opérations sur le domaine infini représenté sont calculées en une seule étape d'évaluation plutôt que d'appliquer de nombreuses règles de réécriture. Nous avons alors adapté la complétion d'automates d'arbres à ce nouveau type d'automate, et la généricité du nouvel algorithme permet de brancher de nombreux treillis abstraits. Cette technique a été implémentée dans un outil appelé TimbukLTA, et cette implémentation permet de démontrer l'efficacité de cette technique.

Alors qu'Anatole France (1844-1924) est considéré comme écrivain sceptique et ironique, un de ses contes intitulé " Le Jongleur de Notre-Dame " échappe à une telle définition. Le ton pieux et sincère de ce conte, fondé sur une légende du Moyen Âge, semble aller à l'encontre du scepticisme, de l'anticléricalisme, et du classicisme déclarés de l'auteur. Au lieu de tenir pour exceptionnels ce type de textes qui mettent en scène une forme de " pureté " dans un sens religieux, tenter de les intégrer dans l'œuvre d'A. France permettra de découvrir une nouvelle facette de l'écrivain, et d'appréhender son idée et son œuvre dans une complexité et une profondeur qui sont cachées sous une apparence simple. Dans un premier temps, on mettra en relation les thèmes médiévaux chez A. France et la mode du médiévisme au XIXe siècle, tant dans le domaine scientifique que dans le courant littéraire, afin d'éclairer l'influence de son époque sur son image médiévale, et la signification de cette image. Dans un deuxième temps, on traitera de la pratique de la réécriture. Par une comparaison, d'une part, entre les textes d'A. France et leurs hypotextes, et d'autre part, entre la réécriture francienne et la réécriture chez les écrivains contemporains, on précisera les caractéristiques et les procédés de la réécriture de notre écrivain. En outre, on montrera que la mise en cadre, ainsi que la réécriture, s'impose dans ses textes, soulignant ainsi la modestie de l'auteur, et la diminution de l'autorité auctoriale. Toutes ces analyses révèleront l'importance de la " simplicité " qui apparaît à plusieurs niveaux dans les textes franciens, et qui peut donner accès à une " pureté " harmonieuse.

Comme dans de nombreux autres domaines, la construction des applications en Informatique Ambiantes (IAm) se fait par réutilisation d'entités logicielles disponibles. Pour des raisons de conductivités, de pannes, de charge de batterie mais aussi de nombreuses autres, la disponibilité de ces entités est imprévisible ce qui implique que l'auto-adaptation dynamique des applications est une nécessité. Cela passe par la spécification en parallèle des adaptations par des experts de divers domaines. Ce parallélisme de construction, peut amener des problèmes d'interférences lors de la composition dynamique de plusieurs adaptations. Dans cette thèse, par l'utilisation de graphes, nous contribuons à la définition d'un cadre formel pour la détection et la résolution de ces interférences. L'assemblage des entités logicielles repose sur des connecteurs d'assemblage qui sont utilisés dans la spécification des adaptations. Des règles de réécriture de graphe permettront de résoudre les interférences détectées, cette résolution étant guidée par la connaissance de connecteurs définis. De plus, pour pouvoir étendre dynamiquement et automatiquement notre mécanisme de gestion des interférences, nous proposons la modélisation comportementale de ces connecteurs. Ceci permet de ne pas reposer sur une connaissance à priori des connecteurs et autorise par la même d'étendre dynamiquement l'ensemble des connecteurs disponibles pour la spécification des adaptations.