Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.

Notre mémoire prend pour objet d’étude les dix-sept textes brefs rassemblés dans le recueil Contes et nouvelles suivis du Théâtre, écrits durant la période symboliste et dans lesquels on constate un phénomène d’hybridation entre les genres narratif et dramatique ainsi qu’entre thèmes symbolistes et décadents. Le premier chapitre s’attache à l’étude de Contes et nouvelles suivis du Théâtre dans la perspective des poétiques du recueil afin de constituer les éléments qui en font une « anthologie de l’entre-deux » du corpus rachildien de textes brefs. En adoptant la perspective de la poétique des genres, il sera question dans le deuxième chapitre d’étudier l’hybridation des genres littéraires, plus précisément entre la prose narrative et le texte dramatique, donnant lieu à des textes en « prose dramatique » qui se situent entre texte à lire et à mettre en scène. Enfin, dans le troisième chapitre nous examinerons les thèmes et les motifs récurrents de l’imaginaire rachildien où s’entremêlent symbolisme et décadentisme, après nous être intéressée à « l’écriture artiste » sous la plume de Rachilde, qui permet de rendre « visibles » les différentes formes de spectres, d’illusions et d’ombres qui parsèment les textes de Contes et nouvelles suivis du Théâtre. / Since Rachilde is generally associated with the french Decadent mouvement, few people are informed that the author also contributed to the symbolist movement of the 1890’s by helping in the set-up of the Théâtre de l’Art and Théâtre de l’Œuvre and especially by composing plays, tales and short-stories which take part in the symbolist spirit of the late nineteenth century. Gathered in the collection Contes et nouvelles suivis du Théâtre published in 1900 by the Mercure de France, these seventeen texts written between 1890 and 1900 establish an anthology of what we call Rachilde’s "symbolist period" of short-story, tale and play writing. Our dissertation is interested in the phenomenon of hybridisation between narrative and dramatic genres as well as between decadent and symbolist themes in this collection little known amongst scholars and the general public. The first chapter of our dissertation becomes attached to the study of Contes et nouvelles suivis du Théâtre in the perspective of the poetics of the collection and examines how the combination of Rachilde’s texts leads to an "anthologie de l’entre-deux". In our second chapter, we adopt the viewpoint of the poetics of genre to discuss the hybridisation of literary genres in Contes et nouvelles suivis du Théâtre, more precisely the narrative and the dramatic genres, that result in "dramatic prose". Finally, in the third chapter, we shall examine the recurring themes of Rachilde’s writing, that entangles decadent and symbolist themes, after being interested in "le style artiste", which allows her to sketch "in a visible way" the various forms of spectres, illusions and shadows that strew the texts of Contes et nouvelles suivis du Théâtre.

Cette thèse présente un modèle générique d'écrans de filets pare-blocs sous sollicitations dynamiques de type impacts. Ces ouvrages pare-blocs sont décrits comme un assemblage abstrait de leurs principaux constituants. Le modèle développé permet ainsi de représenter la plupart des technologies existantes. Un code de calcul en C++ utilisant une Méthode aux Éléments Discrets est développé afin de réaliser les simulations numériques d'impacts. La description générique des ouvrages est mise en œuvre au niveau du code de calcul grâce à une structuration des données et une programmation orientée objet correspondantes. Le modèle générique est complété par deux modèles mécaniques de constituants. Dans un premier temps, un modèle mécanique de filet à anneaux à 4 contacts est développé. Ce modèle est calibré et validé par une campagne expérimentale réalisée sur des anneaux en acier utilisés dans les écrans de filets. Dans un second temps, un modèle général de câble glissant est développé pour modéliser le phénomène d'effet rideau. Ce modèle démontre de fortes capacités de description des phénomènes de glissement et de très bonnes performances de calcul. Enfin, des essais d'impact en vraie grandeur sur deux écrans de filets de technologies différentes sont utilisés afin de valider le modèle générique. Les simulations numériques de ces essais sur ouvrages réels mettent en évidence la pertinence du modèle développé. Les résultats numériques sont en très bon accord avec les expérimentations et le modèle présente des capacités prédictives pertinentes dans la perspective d'usage en ingénierie. Les déformations, les temps de chargement et l'intensité des efforts sont obtenus avec des erreurs inférieures à 10 %. Des simulations complexes d'impacts répétés sont réalisées pour la première fois et le comportement lors de l'impact et pendant la phase de retour élastique après impact est bien appréhendé par le modèle. / This thesis introduces a generic model of rockfall barriers under impact loading. The structures are described as an abstract assembly of their main components. The developed model thereby enables the consideration of most of the existing technologies. A C++ code based on the Discrete Element Method is developed in order to perform the numerical simulations of impacts. The generic description of the barriers is implemented at the code level using a corresponding data structure and object-oriented programming. The generic model is completed by the mechanical models of two components. First, a mechanical model of 4-contact interlaced ring nets is developed. An experimental campaign is carried out to calibrate and validate the model against steel wire rings used in rockfall restraining nets. Second, a general sliding cable model is developed to account for the curtain effect. This model demonstrates great capabilities in describing sliding phenomena and a low computational cost. Finally, full-scale impact tests performed on two barriers of different technologies are used to validate the generic model. Numerical simulations of the full-scale tests highlight the relevance of the developed model. Numerical results agree finely with experiments and the model exhibits compelling predictive capacities for engineering applications. Deformations, loading time and forces magnitude are all predicted within 10 % relative error. Complex and unprecedented simulations of repeated impacts are carried out and the model is able to reproduce the barrier behavior both during the impact phase and after springback.

Support, à l'origine, d'une genèse à la fois textuelle et intellectuelle, lieu mémoriel par excellence, le carnet développe aussi, grâce aux conditions d'écriture spécifiques qu'il favorise, une poétique de l'attention et du regard dont découlent directement écriture de l' « incident » (Barthes) et saisies de l'instant. La discontinuité formelle qu'elles engendrent, en évinçant l'écriture du Moi au profit de l'écriture du Monde, semblent, d'autre part, encourager une poétique de l'anti-journal – perceptible autant d'un point de vue métatextuel que formel. Dans le carnet, de surcroît, se déploient des etha spécifiques et complexes, fondés sur une dialectique subtile entre le « dedans » et le « dehors ». Enfin, la question de la mise en livre du carnet doit être interrogée, sous l'angle de sa publication autant que sa réception : quel protocole éditorial privilégier ? Quel lecteur pour le carnet d'écrivain ? / Originally a medium of genesis, both textual and intellectual, an archetypal memory space, the notebook also develops, thanks to the specific writing conditions it favorises, the poetics of attention and regard from which « incident » (Barthes) style and seizure of the moment style emanate directly. The formal discontinuity that these styles create, World writing rather than writings of Self, seems, on the other hand, to encourage the poetics of the anti-journal – perceptible from both the metatextual and formal points of view. Moreover, in the notebook, specific and complex etha unfold, based upon subtle dialectics situated between the « in » and the « out ». Finally, the question of transforming a notebook into a book has to be asked, from the angle of publication as well as in it's reception : which editorial protocol should be priviledged ? What type of reader for a writer's notebook ?

Les systèmes dits Sensor Webs sont des middlewares informatiques assurant la communication entre les capteurs et les applications. En tant que véritables médiateurs, la popularité de ces systèmes n’a cessé de grandir depuis l’apparition des tout premiers capteurs. Plus récemment, l’émergence de nouveaux paradigmes tels que l’Internet des Objets (IoT) a complètement révolutionné les systèmes basés sur les capteurs en général. Parmi eux, les Sensor Webs ne dérogent pas à cette règle et doivent désormais répondre à de nouveaux défis, notamment en termes d’intégration, de Qualité des Observations (QoO) et d’adaptation système. Dans ce travail de recherche, nous proposons une nouvelle génération de Sensor Webs capables d’adapter la QoO distribuée de manière autonomique et de manière spécifique à chaque application (QASWS). Premièrement, nous introduisons un framework générique destiné aux chercheurs et développeurs souhaitant concevoir leur propre solution QASWS. Dans un deuxième temps, nous instancions ce framework et proposons un prototype de plateforme d’intégration pour l’évaluation de la QoO à la demande (iQAS). Après avoir évalué ses performances, nous présentons trois cas d’utilisation pour la plateforme iQAS. Finalement, nous concluons cette étude en imaginant l’apport de certains paradigmes transverses vis-à-vis de la QoO dans un futur proche. / Sensor Web systems are computer middlewares that aim at bridging the gap between sensors and applications. As true mediators, the popularity of such systems has steadily grown since the appearance of the very first sensors. More recently, the emergence of new paradigms such as the Internet of Things (IoT) has completely revolutionized the sensing research field. As a consequence, Sensor Webs should now cope with new challenges pertaining to integration, Quality of Observation (QoO) and system adaptation. In this research work, we propose a novel generation of Sensor Webs able to adapt the delivered QoO in an autonomic and application-specific manner (QASWS). First, we introduce a generic framework intended for researchers and developers who want to conceive their own QASWS solution. Then, we instantiate this framework and propose a prototype of an integration platform for QoO assessment as a service (iQAS). After evaluating its performances, we present three use cases for the iQAS platform. Finally, we conclude this work by foreseeing the benefits of some transverse paradigms with regard to QoO in the near future.

Les convertisseurs d'électronique de puissance sont de plus en plus exploités notamment dans les applications nécessitant la variation de vitesse de machines. L'utilisation de composants plus performants et plus puissants couplés à de nouvelles structures multiniveaux autorise l'accès à de nouveaux champs applicatifs, ou des fonctionnements à plus haut rendement. Ces convertisseurs statiques sont capables de gérer, par un pilotage adapté, les transferts d'énergie entre différentes sources et différents récepteurs selon la famille de convertisseur utilisée. Au sein de l'interface de pilotage, un schéma particulier permet de générer des signaux de commande pour les interrupteurs, il s'agit de la modulation et peut être vue par deux approches différentes : L'approche intersective issue d'une comparaison modulante-horteuse (appelée en anglais carrier based PWM) et l'approche vectorielle où les signaux de pilotage des trois bras de ponts sont considérés comme un vecteur global unique (appelée Modulation Vectorielle SVM). Le but de la MLI est de générer une valeur moyenne de la tension la plus proche possible du signal modulé. La commande usuelle par comparaison modulante-porteuse dans le cas des architectures multiniveaux nécessite autant de porteuses triangulaires qu'il y a de cellules à commander au sein d'un bras. Plus généralement, la stratégie de modulation de chacune des topologies multiniveaux est choisie en se basant sur des critères à optimiser liés à la qualité les formes d'ondes produites ou obtenues, suite à la conversion. Le choix de la variable de commande à implémenter dans le schéma MLI fait appel à l'expertise de l'expérimentateur et se réfère peu au modèle mathématique initial qui peut-être établit pour caractériser le fonctionnement de l'architecture d'électronique de puissance. En ce qui concerne les stratégies vectorielles SVM, une absence de modèle compatible avec les modèles, basés sur une comparaison modulante porteuse, d'onduleurs est constatée. Les types d'onduleurs triphasés à deux ou à N niveaux de tension admettent un modèle sous forme d'équations d'un système linéaire compatible qui s'écrit sous la forme V = f(a) dans le cas d'une MLI sinusoïdale et V = f(1) dans le cas d'une SVM, avec V les tensions de phase, a les rapports cycliques et f les instants de commutation. Dans cette configuration basique il est constaté que la matrice liant ces tensions aux rapports cycliques (ou aux instants de commutation) n'admet pas d'inverse, ce qui revient à dire qu'il n'est pas possible, avec les théories usuelles des fonctions linéaires, de résoudre ce système afin d'exprimer les rapports cycliques (ou les instants de commutation) en fonction des tensions de références. C'est ce qui explique qu'aujourd'hui un bon nombre d'implémentations pratiques de modulation se fait, suite à une analyse expérimentale des conséquences d'un choix de stratégie sur les variables d'intérêt. / The power electronic converters are increasingly exploited in particular in applications requiring variable speed machines. The use of more effcient and more powerful components coupled with new multilevel structures widens the fields of application and allows high efficiency functioning. These converters are able to manage, with a suitable control, the energy transfer between different sources and different receivers depending on the used converter family. In the control interface, a particular pattern is used to generate control signais for the switches, it is the modulation. Generally, the modulation strategy takes two forms : a Modulation based on comparaison modulating - caiTier (Carrier based Pulse Width Modulation, (CPWM)) or a Vector Modulation (SVM). The purpose of the PWM is to generate a signal which has a mean value as nearest as possible to the desired sinusoidal signal. The usual control by PWM, in the case of multi-level architectures, requires as many triangular carriers as there are cells to be controlled within an arm. The modulation strategy selection for each multilevel topology is based on optimizing criterias related to the quality of the produced waveforms after the conversion. The choice of the variable to implement in the PWM scheme requires expertise of the experimenter and refers little to the initial mathematical model that can be established to characterize the operation of the power electronics architecture. Concerning the vector strategies SVM, the lack of a compatible model with PWM inverters is observed. The three-phase inverters with two or N voltage levels can be modeled in the form of equations of a compatible linear system that is written as V= f(a) in the case of a sinusoïdal PWM and V= f(1) in the case of SVM, with V represents phase voltages, ais a duty cycle and fthe switching instants. In this basic configuration, it is found that the matrix linking these voltages duty cycles (or switching times) adrnits no inverse, which means that it is not possible with the usuallinear functions theories to solve this system in order to express the duty ratios (or the instants of switching) as a function of the reference voltages. This is the reason that today a number of practical implementations of modulation is done after experimental analysis of the consequences of strategy choices on the variables of interest. This study proposes the development of a generic formulation for the modeling of voltage inverters and especially multilevel inverters. The development of generic models for the implementation of modulation strategies is illustrated. The extension of the average model to the three-phase systems is performed to the usual structures of N levels such as the floating capacity and H bridge inverters. The idea is to generalize the model to the multi-level architectures, whether by the sinusoidal PWM modulation expressing the alpha as an output variable, or by the SVM expressing tau. This thesis aims to define a modeling approach and mathematically express the set of solutions in order to generate modulation strategies for various architectures of inverters studied. This will be done using a tool for solving linear systems. This resolution is based on finding degrees of freedom, to be identified at first, then express them in a second step by establishing the link with the criteria to optimize for given architectures. Two examples of application have been implemented on conventional two levels of voltage inverters and the thtree levels flying capacitor voltage inverter.

Made available in DSpace on 2014-06-11T19:26:51Z (GMT). No. of bitstreams: 0 Previous issue date: 2008-12-17Bitstream added on 2014-06-13T19:26:58Z : No. of bitstreams: 1 caron_ec_me_assis.pdf: 397770 bytes, checksum: ad2a9ab1395df97255150f920ef2bc49 (MD5) / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / O doente Molière (2000), de Rubem Fonseca (1925 - ), est un roman racontant les événements qui ont marqué la vie et surtout la mort du dramaturge français Molière (1622-1673). Le récit est fait par son ami le Marquis, qui préfère se maintenir anonyme: il se voit torturé par sa conscience, pour s’être longtemps tu à propos de la possibilité d’empoisonnement de l’auteur de Le malade imaginaire (1673), et décide maintenant d’éclairer le prétendu meurtre. Si l’on observe les recours employés dans l’écriture de ce roman, on constate la présence de plusieurs éléments qui nous permettent de l’envisager comme ce que Linda Hutcheon nomme le roman historique post-moderne (1991), parmi lesqueles on peut citer les suivants: la présence de l’hybridité générique, puisqu’il s’agit d’un roman qui mélange le théâtre, les récits policier et historique; la métafiction – car le narrateur fait constamment allusion au processus de production de l’oeuvre et raconte un événement basé sur l’histoire; la parodie des genres – il y a une subversion générique nette, ainsi que la présence de l’intertextualité avec plusieurs auteurs, notamment avec les oeuvres de Molière, puisque le roman suppose Le malade imaginaire comme sa source de motivation, outre d’autres pièces importantes dans la carrière du dramaturge. Et il y a encore plusieurs citations des Essais de Michel de Montaigne (1580) qui méritent aussi notre attention. / O doente Molière (2000), de Rubem Fonseca (1925 - ), é um romance que narra os acontecimentos que marcaram a vida e que circundaram a morte do dramaturgo francês Molière (1622-1673). A narrativa é feita por seu amigo marquês, que prefere se manter anônimo: ele se sente torturado por sua consciência, por se ter calado durante muito tempo a respeito da possibilidade de envenenamento do autor de Le malade imaginaire (1673), e decide agora esclarecer o pretenso assassinato. Observando os recursos utilizados na escritura deste romance, constatamos vários elementos que nos permitem vê-lo como o que Linda Hutcheon chama de romance histórico pós-moderno (1991), sendo que alguns deles são os seguintes: há presença de hibridismo genérico, já que se trata de um romance que mescla teatro, narrativa policial e histórica; a metaficção – dado que o narrador alude constantemente ao processo de produção da obra e conta um acontecimento baseado na história; a paródia dos gêneros – há uma nítida subversão genérica, assim como a presença do procedimento intertextual, principalmente com as obras do dramaturgo Molière, já que o romance tem como substrato motivador Le malade imaginaire, além de outras peças importantes da carreira do dramaturgo. Além disso, merecem também a nossa atenção as citações provenientes dos Essais de Michel de Montaigne (1580).

Cette étude a pour objet de démontrer la possibilité d'existence de droits sur des choses de genre, c'est-à-dire sur des choses définies de manière générale et d'exposer ensuite ses implications. Cette hypothèse est traditionnellement écartée par la théorie des biens, qui n'admet l'existence de droits de propriété et de droits réels que sur des choses individuellement déterminées. Le principe d'une réservation de choses génériquement déterminées est pourtant concevable et mérite, dans ces conditions, être reconnu. Les conséquences principales de cette reconnaissance sont au nombre de deux. Les droits sur choses de genre présentent tout d'abord la particularité de pouvoir survivre à la confusion de la chose qui constitue leur assiette. Ils présentent également la particularité plus remarquable de pouvoir, dans un assez grand nombre d'hypothèses, survivre à la disparition matérielle ou juridique de la chose qui en constitue l'objet. / The purpose of this study is to demonstrate the possibility of existence of rights over generic things, i.e things whose constitution is determined in consideration of generic features, and to present its implications. Property law has, historically, never admitted the fact that a right could be established on things other than those which are individually determined, and can be refered to as "this" thing. Rights over generic things are, nevertheless, a reality and therefore deserved to be recognized. They have two main characteristics. First of all, they have the ability to survive the mixing of their object with other identical things. They can also, in a rather important number of cases, survive the material or juridical loss of their object.

Le système PLM est l’un des outils stratégiques de l’entreprise. Ces systèmes sont sujets à des changements récurrents dans l’entreprise. Les évolutions organisationnelles, le changement de l’offre produit ou encore le remplacement de logiciels PLM peuvent déclencher l’évolution du système d’information PLM. Une des structures les plus importantes dans les systèmes PLM est le modèle du produit, autour duquel s’articule les informations et processus. C’est autour du modèle produit que se concentrent nos recherches. Les causes d’évolution des modèles produits sont des éléments signifiants qui différencient les étapes de la démarche à suivre. Les méthodes d’IDM sont utilisées afin de formaliser la transformation des modèles. En plus, cette démarche bénéfice d’un cadre de similarité spécialement développé pour la configuration de produit. Un exemple industriel est illustré et résolu en appliquant cette démarche. Il s’agit de l’évolution d’un système gérant les modèles spécifiques de produit vers un système qui est capable de construire et d’utiliser les modèles génériques de produit. Un outil informatique support à nos travaux est développé dans le cadre d'Eclipse. / PLM systems are among the strategic components of enterprise’s information system architecture. These systems undergo frequent evolutions of enterprise. Organizational evolution or product offer variation as well as PLM application replacement may launch PLM systems’ evolution.One of the important structures in PLM systems is the product configuration, which organize and structure all product’s information and processes. Our research activities concern product model evolution. Reasons of product model evolution specify the appropriate methodology and necessary steps in order to handle it. MDE methods are used to formalize the model transformation process.Moreover, our methodology contains a specific similarity framework dedicated to product configuration. An industrial example was illustrated and resolved by this methodology. The problematic of this example is the migration of a system which manage only specific product configuration to a new system that is capable to construct and use generic models of product.

Orientador: Maria Lídia Lichtscheidl Maretti / Banca: Margarida da Silveira Corsi / Banca: Ana Maria Carlos / Resumo: O doente Molière (2000), de Rubem Fonseca (1925 - ), é um romance que narra os acontecimentos que marcaram a vida e que circundaram a morte do dramaturgo francês Molière (1622-1673). A narrativa é feita por seu amigo marquês, que prefere se manter anônimo: ele se sente torturado por sua consciência, por se ter calado durante muito tempo a respeito da possibilidade de envenenamento do autor de Le malade imaginaire (1673), e decide agora esclarecer o pretenso assassinato. Observando os recursos utilizados na escritura deste romance, constatamos vários elementos que nos permitem vê-lo como o que Linda Hutcheon chama de romance histórico pós-moderno (1991), sendo que alguns deles são os seguintes: há presença de hibridismo genérico, já que se trata de um romance que mescla teatro, narrativa policial e histórica; a metaficção - dado que o narrador alude constantemente ao processo de produção da obra e conta um acontecimento baseado na história; a paródia dos gêneros - há uma nítida subversão genérica, assim como a presença do procedimento intertextual, principalmente com as obras do dramaturgo Molière, já que o romance tem como substrato motivador Le malade imaginaire, além de outras peças importantes da carreira do dramaturgo. Além disso, merecem também a nossa atenção as citações provenientes dos Essais de Michel de Montaigne (1580). / Résumé: O doente Molière (2000), de Rubem Fonseca (1925 - ), est un roman racontant les événements qui ont marqué la vie et surtout la mort du dramaturge français Molière (1622-1673). Le récit est fait par son ami le Marquis, qui préfère se maintenir anonyme: il se voit torturé par sa conscience, pour s'être longtemps tu à propos de la possibilité d'empoisonnement de l'auteur de Le malade imaginaire (1673), et décide maintenant d'éclairer le prétendu meurtre. Si l'on observe les recours employés dans l'écriture de ce roman, on constate la présence de plusieurs éléments qui nous permettent de l'envisager comme ce que Linda Hutcheon nomme le roman historique post-moderne (1991), parmi lesqueles on peut citer les suivants: la présence de l'hybridité générique, puisqu'il s'agit d'un roman qui mélange le théâtre, les récits policier et historique; la métafiction - car le narrateur fait constamment allusion au processus de production de l'oeuvre et raconte un événement basé sur l'histoire; la parodie des genres - il y a une subversion générique nette, ainsi que la présence de l'intertextualité avec plusieurs auteurs, notamment avec les oeuvres de Molière, puisque le roman suppose Le malade imaginaire comme sa source de motivation, outre d'autres pièces importantes dans la carrière du dramaturge. Et il y a encore plusieurs citations des Essais de Michel de Montaigne (1580) qui méritent aussi notre attention. / Mestre