Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Cette thèse s'intéresse à la démonstration automatique de la validité de formules mathématiques issues de la preuve de programmes. Elle se focalise tout particulièrement sur la Satisfiabilité Modulo Théories (SMT): un jeune domaine de recherche qui a connu de grands progrès durant la dernière décennie. Les démonstrateurs de cette famille ont des applications diverses dans la conception de microprocesseurs, la preuve de programmes, le model-checking, etc.Les démonstrateurs SMT offrent un bon compromis entre l'expressivité et l'efficacité. Ils reposent sur une coopération étroite d'un solveur SAT avec une combinaison de procédures de décision pour des théories spécifiques comme la théorie de l'égalité libre avec des symboles non interprétés, l'arithmétique linéaire sur les entiers et les rationnels, et la théorie des tableaux.L'objectif de cette thèse est d'améliorer l'efficacité et l'expressivité du démonstrateur SMT Alt-Ergo. Pour cela, nous proposons une nouvelle procédure de décision pour la théorie de l'arithmétique linéaire sur les entiers. Cette procédure est inspirée par la méthode de Fourier-Motzkin, mais elle utilise un simplexe sur les rationnels pour effectuer les calculs en pratique. Nous proposons également un nouveau mécanisme de combinaison, capable de raisonner dans l'union de la théorie de l'égalité libre, la théorie AC des symboles associatifs et commutatifs et une théorie arbitraire deShostak. Ce mécanisme est une extension modulaire et non intrusive de la procédure de completion close modulo AC avec la théorie de Shostak. Aussi, nous avons étendu Alt-Ergo avec des procédures de décision existantes pour y intégrer d'autres théories intéressantes comme la théorie de types de données énumérés et la théorie des tableaux. Enfin, nous avons exploré des techniques de simplification de formules en amont et l'amélioration de son solveur SAT. / This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on Satisfiability Modulo Theories (SMT): a young research topic that has seen great advances during the last decade. The solvers of this family have various applications in hardware design, program verification, model checking, etc.SMT solvers offer a good compromise between expressiveness and efficiency. They rely on a tight cooperation between a SAT solver and a combination of decision procedures for specific theories, such as the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, or the theory of arrays.This thesis aims at improving the efficiency and the expressiveness of the Alt-Ergo SMT solver. For that, we designed a new decision procedure for the theory of linear integer arithmetic. This procedure is inspired by Fourier-Motzkin's method, but it uses a rational simplex to perform computations in practice. We have also designed a new combination framework, capable of reasoning in the union of the free theory of equality, the AC theory of associative and commutativesymbols, and an arbitrary signature-disjoint Shostak theory. This framework is a modular and non-intrusive extension of the ground AC completion procedure with the given Shostak theory. In addition, we have extended Alt-Ergo with existing decision procedures to integrate additional interesting theories, such as the theory of enumerated data types and the theory of arrays. Finally, we have explored preprocessing techniques for formulas simplification as well as the enhancement of Alt-Ergo's SAT solver.

Les langages synchrones tels que Signal, Lustre et Esterel sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de Signal. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé. / Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Cette recherche s’intéresse à l’utilisation du conte dans le domaine de l’enseignement des langues étrangères. Elle s’appuie sur l’analyse d’un échantillon de contes d’origines algérienne et française pour démontrer le potentiel pédagogique de cette forme littéraire. L’analyse de notre corpus a permis de mettre en lumière les diverses exploitations du conte dans le domaine de la didactique des langues. En effet, grâce à son contenu culturel, ce genre littéraire est un excellent médiateur pour initier l’élève à la culture-cible. Nous avons expliqué que le conte était parfaitement adapté pour mener les élèves à prendre conscience des dimensions intertextuelle et interculturelle de l’oeuvre littéraire. En s’appropriant ces deux notions, les apprenants construisent une culture littéraire essentielle pour développer leurs compétences dans les domaines de la lecture et de l’écriture. Le conte permet aussi de proposer des exercices féconds qui concernent les domaines de lecture, d’écriture, ainsi que les aspects linguistiques.L’expérience pédagogique, menée auprès d’un public de collégiens en Algérie, a été l’occasion de valider notre hypothèse sur l’utilité des contes dans le domaine de l’enseignement des langues étrangères. En effet, l’instauration de notre dispositif pédagogique, basé sur l’exploitation d’une série de contes, a conduit les élèves à prendre conscience de l’intérêt de la mise en valeur de leur culture dans le domaine scriptural. L’analyse intertextuelle et interculturelle des contes proposés par les élèves dans la macro-tâche du post-test, indique leur reprise des motifs caractéristiques des contes arabes et européens. De même, nous avons constaté que les élèves avaient amélioré la qualité structurelle de leurs textes. En effet, l’analyse formelle de leurs écrits a permis de conclure que la majorité des apprenants avait produit des contes qui satisfont aux règles de la cohérence textuelle. Ce résultat indique que le conte est un genre qui convient pour conduire les élèves à produire des textes cohérents. Par ailleurs, la macro-tâche a également été un moyen pour vérifier l’évolution de leur compétence linguistique. Plus précisément, l’observation de leurs écrits indique qu’ils ont fait des progrès dans les domaines lexical et morphologique. En revanche, en ce qui concerne la syntaxe, les élèves nécessitent plus d’accompagnement pour maîtriser cet aspect de la langue-cible. / This research focuses on the use of storytelling in the field of teaching foreign languages. It is based on the analysis of a sample of stories from Algerian and French origins to demonstrate the pedagogical potential of this literary form.The analysis of our corpus has made it possible, to highlight the various storytelling operations in the area of language teaching.In fact, because of its cultural content, this literary type represents an excellent mediator to introduce students to the culture-target. We explained that storytelling was perfectly suited to help students become aware of the intertextual and intercultural dimensions of literary work. By appropriating these two concepts, learners build an essential literary culture to develop their skills in the reading and writing fields. Storytelling allows also to offer fruitful exercises in the reading and writing domains, as well as the linguistics aspects. The educational experience, conducted among a college students audience in Algeria, was an opportunity to validate our hypothesis on the usefulness of tales in the field of foreign languages teaching. Indeed, the establishment of our educational system, based on the exploitation of a series of tales, has led students to realize the value of enhancing their culture in the scripture domain.The intertextual and intercultural analysis of the tales proposed by the students in the macro-task of the post-test indicates their resumption of the grounds that are characteristic of the Arabic and European ones. Moreover, we found that students had improved the structural quality of their texts. Indeed, the formal analysis of their writings led to the conclusion that the majority of learners had produced stories that satisfied the rules of textual coherence.This result indicates that storytelling is an appropriate way to lead students to produce coherent texts. Furthermore, the macro-task has also been an efficient way to verify the evolution of their language skills.More specifically, the observation of their writings indicates that they have made progress in the lexical and morphological domains. On the other hand, students need more coaching, for all what is related to syntax, to control this aspect of the target language. / هذا البحث يتناول موضوع استعمال الحكايات في مجال تعليم اللغات الأجنبية. يستند هذا العمل على تحليل مجموعة من الحكايات تنتمي إلى الثقافتين الجزائرية و الفرنسية من أجل إيضاح مختلف الاستعمالات للحكاية في مجال تعليم اللغات الأجنبية. هذا النوع الأدبي يعد وسيلة ممتازة لتنمية معارف التلميذ فيما يتعلق بالثقافة الأجنبية. لقد شرحنا أن الحكاية مناسبة لتوعيته حول البعد التناصيّ و المتعدد الثقافات للنص الأدبي. بإدراكه لهاتين النقطتين، يُكوّن التلميذ ثقافة أدبية أساسية من أجل تنمية كفاءته في مجاليّ القراءة و الكتابة. الحكاية تسمح أيضا باقتراح تمارين خصبة تتعلق بمجالات القراءة، الكتابة و قواعد اللغة.التجربة البيداغوجية التي قمنا بها مع مجموعة من تلاميذ الطور الإكمالي، كانت فرصة لإثبات فرضيتنا حول فائدة الحكايات في مجال تعليم اللغات الأجنبية . استعمال نظام بيداغوجي يستند على مجموعة من القصص قاد التلاميذ لإدراك أهمية استغلال ثقافتهم في مجال الكتابة.التحليل التناصي و المتعدد الثقافات للحكايات المقترحة من طرف التلاميذ في التمرين النهائي يبرز اعادتهم لمقاطع أدبية تنتمي لحكايات غربية و أوروبية. لاحظنا أيضا أنّ التلاميذ اقترحوا حكايات تلتزم بقواعد الترابط النصي. هذه النتيجة تبيّن أنّ الحكاية هي جنس أدبي يناسب لقيادة التلاميذ نحو كتابة نصوص مترابطة. كما أنّ التمرين النهائي كان وسيلة لفحص تطور الكفاءة اللغوية عند التلاميذ الذين قاموا بتطوير مهاراتهم في مجالي اللغة و القواعد. لكن فيما يتعلق بمجال النحو، لقد لاحظنا أنّهم يحتاجون للمزيد من المرافقة حتى يتقنون هذا المجال اللغوي.

Cette thèse est consacrée à l’étude des monoïdes plaxiques par une nouvelle approche utilisant des méthodes issues de la réécriture. Ces méthodes sont appliquées à des présentations de monoïdes plaxiques décrites en termes de tableaux de Young, de bases cristallines de Kashiwara et de modèle des chemins de Littelmann. On étudie le problème des syzygies pour la présentation de Knuth des monoïdes plaxiques. En utilisant la procédure de complétion homotopique basée sur les procédures de complétion de Squier et de Knuth–Bendix, on construit des présentations cohérentes de monoïdes plaxiques de type A. Une telle présentation cohérente étend la notion de présentation convergente d’un monoïde par une famille génératrice de syzygies, décrivant toutes les relations entre les relations. On explicite une présentation cohérente finie des monoïdes plaxiques de type A avec les générateurs colonnes. Cependant, cette présentation n’est pas minimale dans le sens que plusieurs de ses générateurs sont superflus. En appliquant la procédure de réduction homotopique, on réduit cette présentation en une présentation cohérente finie qui étend la présentation de Knuth, donnantainsi toutes les syzygies des relations de Knuth. D’une manière plus générale, on étudie des présentations de monoïdes plaxiques généralisés du point de vue de la réécriture. On construit des présentations convergentes finies de ces monoïdes en utilisant les chemins de Littelmann. De plus, on étudie ces présentations pour le type C en termes de bases cristallines de Kashiwara. En introduisant les générateurs colonnes admissibles, on construit une présentation convergente finie du monoïde plaxique de type C avec des relations explicites. Cette approche nous permettrait d’étudier le problème des syzygies des présentations de monoïdes plaxiques en tout type / This thesis focuses on the study of plactic monoids by a new approach using methods issued from rewriting theory. These methods are applied on presentations of plactic monoids given in terms of Young tableaux, Kashiwara’s crystal bases and Littelmann path model. We study the syzygy problem for the Knuth presentation of the plactic monoids. Using the homotopical completion procedure that extends Squier’s and Knuth–Bendix’s completions procedure, we construct coherent presentations of plactic monoids of type A. Such a coherent presentation extends the notion of a presentation of a monoid by a family of generating syzygies, taking into account all the relations among the relations. We make explicit a finite coherent presentation of plactic monoids of type A with the column generators. However, this presentation is not minimal in the sense that many of its generators are superfluous. After applying the homotopical reduction procedure on this presentation, we reduce it to a finite coherent one that extends the Knuth presentation, giving then all the syzygies of the Knuth relations. More generally, we deal with presentations of plactic monoids of any type from the rewriting theory perspective. We construct finite convergent presentations for these monoids in a general way using Littelmann paths. Moreover, we study the latter presentations in terms of Kashiwara’s crystal graphs for type C. By introducing the admissible column generators, we obtain a finite convergent presentation of the plactic monoid of type C with explicit relations. This approach should allow us to study the syzygy problem for the presentations of plactic monoids for any type

(Résumé en français) "Exercices de style" est-elle une oeuvre simplement comique et acrobatique ? Sa réception positive mais plutôt superficielle auprès du public semble avoir dissimulé ses aspects plus profonds et plus problématiques. A nos yeux, en revanche, les 99 "Exercices" d'écriture sont tout à fait aptes à éclairer les problèmes essentiels de la création littéraire et de la transmission de l'énoncé qu'est la communication verbale. La structure multi-dimensionnelle du livre, où les "Exercices" s'enchaînent, se complètent et se répondent, nous rend sensibles non seulement aux réseaux intratextuels qu'entretiennent les "Exercices", mais également aux liens intertextuels qui lient cetains d'entre eux et les discours littéraires et non littéraires préexistants. D'autres "Exercices" témoignent du regard autoréflexif de l'écrivain, ceux qui peuvent être considérés comme autoparodie. Par ailleurs, la virtuosité des variations stylistiques exige parfois du lecteur une attention particulière - face à quelques variations hermétiques et presque inintelligibles, on devra recourir à d'autres composants du livre qui serviront de "traductions". La terme "traduction" devra être compris non seulement dans le sens de la transmission de messages entre différentes langues, mais aussi dans le sens de la transposition d'un signifiant dans d'autres signifiants, ou bien de la "réécriture" d'un énoncé, tout en restant dans la même langue. Si le principe des "Exercices de style" est de renouveler à l'infini des exercices d'écrire, ou plutôt de réécrire LE texte original - "qui est d'ailleurs inexistant" -, nous pouvons poser, semble-t-il, que la Littérature est basée sur le même procédé de tâtonnements,auquel le lecteur est enctraîné à participer. (Abstract in English) Is "Exercises in style" just a comic and acrobatic book ? The fact that the readers welcomed it so favourably - but rather superficially - seems to have overshadowed its more serious and problematic aspects. In our opinion indeed, Queneau's ninety-nine writing "Exercises" can clearly shed light on the essential problems of literary creation and utterance transmission, i.e. verbal communication. The book presents an intricate structure:the "Exercises" are linked together, echo each other and complement one another. Through this multidimensional structure, we can see the intratextual networks between the "Exercises" as well as their intertextual relations with pre-existent literary and non-literary discourses. Other "Exercises" show the author's autoreflective, autoparodic attitude. Furthermore, the virtuosity of the stylistic variations sometimes requires particular attention from the reader. To understand some abstruse, sometimes almost unintelligible "Exercises", the reader has to resort to other parts of the book, which will serve as "translation" for these enigmatic passages. The word "translation" here means not only transmission of messages from a language to another, but also transposition of a signifier to other signifiers - in other words, "rewriting" of an utterance in the same language. If the principle of "Exercices in style" is to practice writing endlessly, or rather rewriting of THE original text - "which actually does not exist" - , we can reasonably deduce that Literature is based on the same trial and error process the reader will inevitably take part in.

“Telling Otherwise: Rewriting History, Gender, and Genre in Africa and the African Diaspora” examines counter-discursive postcolonial rewritings. In my first chapter, “Re-Writing the Canon,” I examine two works that rewrite canonical texts from the European tradition, Jean Rhys’s retelling of the life of Jane Eyre’s Bertha in Wide Sargasso Sea and Maryse Condé’s relocation of Wuthering Heights to the Caribbean in La migration des coeurs. In this chapter, I contend that re-writing functions not only as a response, as a “writing back” to the canon, but as a creative appropriation of and critical engagement with the canonical text and its worldview. My second chapter, “Re-Storying the Past,” examines fictional works that rewrite events from the historical past. The works that I study in this chapter are Assia Djebar’s recuperation of Algerian women’s resistance to French colonization in L’amour, la fantasia and Edwidge Danticat’s efforts to reconstruct the 1937 massacre of Haitians under Trujillo in The Farming of Bones. In my third chapter, “Re-Voicing Slavery,” I take for my subject neo-slave narratives that build on and revise the slave narrative genre of the late eighteenth- through early twentieth- centuries. The two works that I examine in this chapter are Sherley Anne Williams’s Dessa Rose and the poem sequence Zong! by M. NourbeSe Philip, based on the 1781 murder of Africans aboard the slave ship Zong. My fourth chapter, “Re-Membering Gender,” examines texts that foreground the processes of re-writing and re-telling, both thematically and structurally, so as to draw attention to the ways in which discourses and identities are constructed. In their attempts to counter masculinist discourses, these works seek to re-inscribe gender into these discourses, a process of re-membering that engenders a radical deconstruction of fixed notions of identity. The works that I read in this chapter include Daniel Maximin’s L’Isolé soleil, which privileges the feminine and the multiple in opposition to patriarchal notions of single origins and authoritative narrative voices and Maryse Condé’s Traversée de la Mangrove, which rewrites Patrick Chamoiseau’s novel Solibo Magnifique so as to critique the exclusive nature of Caribbean identity in his notion of créolité. / text

No description available.

Ce document présente l'étude de plusieurs modèles de machines à états finis qui étendent tous le même formalisme: les automates d'arbres classiques, et leur application dans différentes tâches telles que l'analyse statique de programmes ou de systèmes, la typage, la vérification de la cohérence de spécifications, le model checking... Les arbres sont une structure naturelle de données, très répandue en informatique, par exemple pour la représentation des structures de données hiérarchiques ou imbriquées, pour des algorithmes spécifiques (arbres binaires de recherche, algorithmes distribués), comme modèle abstrait pour des données semi-structurées utilisées pour l'échange d'information dans le Web, pour une présentation algébrique de processus récursifs, comme les termes en logique... Lorsqu'il s'agit de raisonner sur des systèmes manipulant des arbres, ou modelisés par des arbres, il est crucial d'avoir une représentation finie d'ensembles infinis d'arbres. Les automates d'arbres sont des machines à états finis permettant une telle représentation. Ils ont fait la preuve de leur adéquation à des tâches de raisonnement: ils ont un modèle théorique bien établi, en étroite relation avec la logique, ils bénéficient de bonnes propriétés de composition et d'algorithmes de décision efficaces. En particulier, les automates d'arbres sont utilisées au coeur de systèmes de vérification formelle d'outils de déduction automatique. Toutefois, les automates d'arbres ont des limitations sévères en expressivité. Par exemple, ils sont incapables de faire du filtrage non-linéaire ou d'exprimer des contraintes d'intégrité tels que les clés dans les bases de données. Certaines extensions ont été proposées afin d'améliorer le modèle en essayant de conserver de bonnes propriétés. Nous présentons dans ce document de plusieurs de telles extensions, leurs propriétés et leur utilisation en vérification symbolique de systèmes et de programmes.

[pt] Esta tese apresenta uma análise de reescritas brasileiras dos contos de Charles Perrault, sob uma perspectiva diacrônica e sincrônica, com o objetivo de compreender as diferentes formas como os contos do autor francês do século XVII têm sido reescritos no sistema literário brasileiro. Publicada na França, em 1697, a obra Histórias ou Contos do tempo antigo com moralidades ou Contos de Mamãe Gansa, alçada posteriormente à categoria de clássico da literatura infantojuvenil, contém oito contos em prosa, seguidos de moralidades em verso ao final de cada narrativa: A Bela Adormecida no bosque, O Chapeuzinho Vermelho, Barba Azul, O Mestre Gato ou o Gato de Botas, As Fadas, A Gata Borralheira ou A Sapatilha de Vidro, Riquete do Topete e O Pequeno Polegar (títulos dos contos de acordo com a tradução de Mário Laranjeira). Nesses contos, ao mesmo tempo em que recupera histórias populares da oralidade, Perrault insere sua marca autoral, a moralidade em verso, comentário final do autor sobre a história contada em prosa. Considerando que as moralidades possuem uma dupla função - autoral e literária - esta pesquisa se volta para o estudo da transmissão dos contos no Brasil com foco nesse duplo aspecto: a questão da autoria e a questão da literariedade. Tendo como principal pilar teórico os Estudos Descritivos da Tradução e adotando a metodologia de Lambert e Van Gorp, o corpus objeto de análise é composto por reescritas (e seus paratextos) publicadas em livro, desde o momento inicial em que os contos surgem no sistema literário brasileiro, ao final do século XIX, até a contemporaneidade, com a mais recente reescrita publicada em 2016. São também examinados alguns metatextos, tais como cartas e entrevistas, que auxiliam na compreensão das propostas dos reescritores e editores das obras. A partir das noções de André Lefevere acerca de reescrita e patronagem, considera-se que reescritas exercem papel central para o estabelecimento e a manutenção de cânones literários e projetam imagens novas ou distintas de obras e autores, de acordo com concepções ideológicas e poetológicas dos responsáveis pelas publicações (reescritores, prefaciadores, editores). Portanto, esta tese propõe a adoção de uma linha de pesquisa para os estudos literários que atente para a centralidade do fator reescrita, quando são analisadas obras estrangeiras inseridas em sistemas literários alvo. Como será visto no caso de Perrault no Brasil, as reescritas mais recentes, com diferenças relevantes em termos literários em relação às reescritas mais antigas, projetam novas imagens da obra e do autor, possibilitando novas leituras por parte do público leitor contemporâneo. / [en] In this doctoral dissertation, Brazilian rewritings of Charles Perrault s tales are analysed from a diachronic and synchronic perspective with the aim of comprehending the different forms in which this seventeenth-century French writer s stories have been rewritten in the Brazilian literary system. Published in France in 1697, Stories or Tales of Bygone Times, with Morals or Tales of Mother Goose, which was later acknowledged as a classic of children s literature, contains eight tales in prose followed by morals in verse at the end of each narrative: The Sleeping Beauty in the Wood, Little Red Riding-Hood, Bluebeard, The Master Cat or Puss in Boots, The Fairies, Cinderella or The Little Glass Slipper, Ricky of the Tuft and Little Thumb (full translations of the titles from the French source text). In these tales, while drawing on popular stories from the oral tradition, Perrault inserts his trademark morals in verse, offering a final comment on the story told in prose. Considering that the morals have a twofold function - both authorial and literary - the transmission of the tales in Brazil is studied with a focus on this dual aspect: authorship and literariness. Taking Descriptive Translation Studies as the main theoretical perspective and adopting Lambert and Van Gorp s methodology, the corpus under analysis is composed of rewritings (and their paratexts) published in books, ranging from when the tales first appeared in the Brazilian literary system in the late nineteenth century to the current day, the most recent of which having been published in 2016. Some metatexts are also examined, such as letters and interviews, which are helpful for understanding the rewriters and editors objectives. Based on Andre Lefevere s theoretical work on rewriting and patronage, it is suggested that rewritings exert a central role in establishing and maintaining literary canons and project new or distinct images of works and authors, according to the poetological and ideological conceptions of the actors responsible for the publications (rewriters, preface writers, editors). Therefore, a proposal is made for the adoption of an approach for research in literary studies that takes account of the centrality of the rewriting factor, in analyses of foreign works in target literary systems. As seen in the case of Perrault in Brazil, the most recent rewritings, which differ significantly in literary terms from the older rewritings, project new images of the work and the writer, making new readings possible for a contemporary readership.