No description available.

La lecture est fréquemment associée dans la modernité à un exercice de l’esprit vers l’acquisition des informations et de savoir. Cette façon de concevoir l’acte de lire comme une action centrée majoritairement sur le mental, toutefois, cache une tradition de lecture amplement corporelle pratiquée entre la basse Antiquité et la fin de la période médiévale. Cette thèse s’occupe d’examiner alors une rupture historique entre corps et lecture, un processus qui sous-tend l’avènement de la façon moderne de lire, c’est-à-dire d’un modèle qui est enraciné dans la vision et dans les fonctions intellectuelles. Ce travail s’appuie sur les études des théoriciens de l’histoire de la lecture, ainsi que sur une ample réflexion sur la sagesse émanée du corps dans le but de récupérer une lecture associée à la pratique synesthésique. Pour accomplir cette tâche, l’on cherche à l’intégration de perspectives historique, analytique et pratique pour discuter et mettre en action une lecture de teneur corporelle. Ceci implique une pratique qui entre aussi dans la dynamique de la thèse. Ainsi, on part de l’analyse de la Poésie Concrète majoritairement brésilienne pour atteindre à deux objectifs à la fois : tout d’abord, on caractérise ce mouvement poétique qui est une référence dans le contexte de la poésie visuelle, ce qui corroborait à l’importance de la vue dans le contexte de l’histoire de la lecture. D’un autre point de vue, le travail de cette thèse avec la Poésie Concrète rend tangible aussi la démonstration d’une force corporelle dans la lecture en action qu’on y apporte. Ainsi, comptant sur une approche de lecture qui est aussi pratique, la thèse vise à démontrer qu’il y a une implication inexorable du corps dans l’acte de lire. / Reading is frequently associated in modernity with a mental practice seeking to acquire knowledge and information. Nevertheless, this way of conceiving reading as an act focused mainly on intellectuality conceals a vast tradition of bodily reading practiced from late Antiquity up to the end of the medieval period. This dissertation thus aims to examine the historical rupture between the body and the reading process underlying the emergence of our modern way of reading, which emphasizes the sense of sight and purely intellectual functions. This research is grounded on theoretical studies of the history of reading, as well as on a broad reflection on knowledge emanating from the body, and thus proposes recovering a reading model associated with synesthetic practice. To accomplish this task, this study seeks to integrate historical, analytical and practical perspectives as a way to discuss and enact a reading method conscious of the body's existence; the role of the body in the act of reading is part and parcel of the dissertation’s dynamic. The analysis of Brazilian Concrete Poetry allows for achieving two objectives at once: first, a characterization of this poetic movement, considered exemplary of visual poetry, corroborates the singular importance of sight in the history of reading in modernity. In addition, however, working with the Concrete Poetry offers a tangible demonstration of the body’s force in the context of interactive reading. In other words, in endorsing an understanding of reading based on practice, the dissertation strives to show how the act of reading implies the irrepressible presence of the body.

Ce mémoire analyse les stratégies employées par Verónica Gerber Bicecci dans son livre La Compañía (La Compagnie, 2019) afin de susciter une réflexion sur l’extractivisme minier au Mexique. La Compañía alerte le lecteur sur les conséquences négatives de considérer la nature, et tout ce qui s’y rapporte, comme passif ou inerte. Cette vision réductrice justifie la surexploitation des biens naturels, qui épuise les écosystèmes dont l’humain dépend en tant qu’espèce, tout en ignorant l’agentivité non humaine, ce qui s’avère problématique lorsqu’il s’agit d’extraire et de manipuler des substances toxiques telles que le mercure. La Compañía, une réécriture de la nouvelle d’Amparo Dávila « El huésped » (1959), réunit des archives textuelles et visuelles pour raconter l’histoire de Nuevo Mercurio (Zacatecas), une ville minière abandonnée. Le livre dépeint une compagnie minière comme un monstre afin de rendre visible le danger qu’elle représente pour les personnes et l’environnement, et présente les réponses inquiétantes de ses victimes, les femmes et la nature, à la violence extractiviste. Entendue en son sens le plus large, la matière passe de la catégorie d’objet à celle de sujet et devient un acteur, faisant apparaître la possibilité de conceptualiser des formes non humaines de résistance à l’extractivisme minier. Une lecture écogothique de La Compañía montre que ces réponses, qui n’ont pas été abordées dans les récits miniers de type réaliste social, exposent les fondements idéologiques du capitalisme extractif. / This research analyses the strategies employed by Verónica Gerber Bicecci in her book La Compañía (The Company, 2019) to raise questions about extractivism in Mexico. La Compañía alerts readers to the negative consequences of viewing nature, and everything related to it, as passive or inert. This reductive vision justifies the overexploitation of natural resources, thereby depleting the ecosystems on which the humans depend as a species, while ignoring non-human agency, which proves problematic when it comes to the extraction and handling of toxic substances such as mercury. La Compañía, a rewriting of Amparo Dávila’s short story “El huésped” (1959), brings together textual and visual archives to tell the story of Nuevo Mercurio (Zacatecas), an abandoned mining town. The book depicts a mining company as a monster to make visible the danger it poses to people and the environment, and presents the disturbing responses of its victims, women and nature, to extractivist violence. The author conceptualizes non-human forms of resistance to extractivism through the agency of matter in its broadest sense, which no longer belongs to the category of object, but instead becomes a subject. An ecogothic reading of La Compañía shows that these responses, which have not been addressed in social realist mining narratives, expose the ideological foundations of extractive capitalism. / Esta investigación analiza las estrategias empleadas por Verónica Gerber Bicecci en su libro La Compañía (2019) para suscitar una reflexión sobre el extractivismo minero en México. La Compañía alerta al lector sobre las consecuencias negativas de considerar la naturaleza, y todo lo relacionado con ella, como pasivo o inerte. Esta visión reductora justifica la sobreexplotación de los bienes naturales, que agota los ecosistemas de los que dependen los humanos como especie, al tiempo que ignora la agencia no-humana, lo cual resulta problemático cuando se trata de extraer y manipular sustancias tóxicas como el mercurio. La Compañía, una reescritura del cuento “El huésped” (1959) de Amparo Dávila, reúne archivos textuales y visuales para contar la historia de Nuevo Mercurio (Zacatecas), un pueblo minero abandonado. El libro retrata una empresa minera como un monstruo para hacer visible el peligro que supone para las personas y el medioambiente, y presenta las respuestas inquietantes de sus víctimas, las mujeres y la naturaleza, a la violencia extractivista. Entendida en su sentido más amplio, la materia pasa de la categoría de objeto a la de sujeto y se convierte en actor, lo que posibilita conceptualizar formas no humanas de resistencia al extractivismo minero. Una lectura ecogótica de La Compañía muestra que estas respuestas, que no se han abordado en las narrativas mineras de tipo realista social, exponen los fundamentos ideológicos del capitalismo extractivo.

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

La plupart des entreprises évoluent dans des marchés concurrentiels en adaptant rapidement leurs processus métiers. Leur performance dépend de leur capacité à utiliser des techniques d'amélioration continue de leur organisation par la mise au point de Systèmes Informatiques (SI) durables pour l'automatisation des processus. En ce sens, les architectures orientées services (Service Oriented Architectures) ont permis le développement de SI flexibles avec un style d'architecture prédominant de composition de services. Cependant, l'alignement de ces architectures aux impératifs de l'évolution des processus reste une préoccupation centrale. Dans cette thèse, nous étudions la cartographie et l'évolution des processus métiers depuis leur conception jusqu'à leur automatisation dans une architecture orientée services ainsi que son adaptation. Nous proposons une approche d'ingénierie dirigée par les modèles intégrée à un outil de modélisation de processus et de développement d'architectures orientées services. Celle-ci débute par la spécification d'un modèle BPMN (Business Process Modeling Notation) décrivant les interactions des processus métiers. Grâce à une chaîne de transformation automatisée, nous produisons un modèle SCA (Service Component Architecture) décrivant une solution de composition de services. Ceci garantit la traçabilité architecturale entre le niveau métier du SI et son niveau technique puisque les services générés décrivent une {logique applicative} qui met en œuvre la logique métier du modèle BPMN. Ensuite, nous introduisons une méthode de propagation du changement de la logique métier vers la logique applicative qui est fondée sur la synchronisation incrémentale entre les modèles BPMN et SCA. Elle est intégrée à un outil d'analyse de l'impact du changement qui se base sur la réécriture de graphes pour éviter les inconsistances induites par les modifications. Enfin, elle permet de simuler l'impact des évolutions des processus, pour en estimer le coût selon les métriques que nous proposons, avant de procéder à la réingénierie de l'architecture orientée services pour assurer une meilleure gouvernance du changement.

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é.

No description available.