Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Partant du sonnet « À une passante » de Baudelaire pour aboutir aux écrits de Breton en parcourant un florilège de textes traitant de la première rencontre, nous avons exploré dans un premier temps les spécificités de la scène poétique relativement à la scène romanesque étudiée par Jean Rousset. Dans un second temps, nous avons cherché à saisir les nouvelles caractéristiques du scénario moderne par rapport aux configurations classique et romantique. En adressant à l’inconnue croisée dans une rue de Paris le poème qu’elle a suscité l’instant d’un coup d’œil fugitif, Baudelaire crée un poncif amoureux nouveau. Dans ce sonnet, le cadre spatio-temporel, les acteurs, la rencontre et l’amour portent l’empreinte de la modernité jusqu’à en devenir l’emblème. D’autres poètes reprendront sur le mode de l’imitation ou de la variation le modèle baudelairien, et notamment la figure de la passante. Le poème de la première rencontre devient alors le lieu de la célébration d’une nouvelle figure féminine mais surtout d’une nouvelle lyrique qui n’est rien de moins qu’une érotique de la distance séparatrice. Chaque poème nous montre à sa façon que l’unique scène signifiante est celle du désir (qui déchire le poète et son lecteur) et que l’écriture d’une rencontre sans issue est l’ultime échappatoire contre l’absence. / Starting from the sonnet "To a passer-by" of Baudelaire to lead to the writings of Breton by traversing a group of texts treating of the first meeting, we initially explored specificities of the poetic scene compared to the romantic scene studied by Jean Rousset. In a second step, we sought to understand the new features of modern scenario compared ti the classical and romantic settings. By sending to unknown crossed in a street of Paris the poem that she aroused the moment all at once of escaped eye, Baudelaire creates a new loving common place. In this sonnet, the spatiotemporal frame, the actors, the meeting and the love carry the imprint of the modernity until become the emblem. Other poets will take back on the mode of simulation or of variation the baudelerian model, and notably the figure of the passer-by. The poem of the first meeting becomes then the place of the celebration of a new feminine figure but especially of the lyric news which is nothing at least than an erotic of dividing distance.

Ce manuscrit présente une réflexion sur la terminaison des systèmes de réécriture d'ordres supérieurs. Nous nous concentrons sur une méthode particulière, la terminaison à base de tailles. La terminaison à base de tailles utilise le typage pourdonner une approximation syntaxique à la taille d'un élément du langage. Notre contribution est double: premièrement, nous permettons d'aborder de manière structurée le problème de la correction des approches à base de taille. Pour ce faire, nous montrons qu'elle peut être traitée par une version de la méthode des annotations sémantiques. Cette dernière utilise des annotations sur les termescalculés à partir de la sémantique des sous-termes dans un certain prémodèle équationnel. Nous montrons la correction de notre approche par annotations sémantiques, ainsi que du critère qui permet de traiter le système annoté, et nous construisons un prémodèle pour le système qui correspond intuitivement à lasémantique du système de réécriture. Nous montrons alors que le système annoté passe le critère de terminaison. D'un autre côté nous modifions l'approche classique de la terminaison à base de tailles et montrons que le système modifiépermet une analyse fine du flot de contrôle dans un langage d'ordre supérieur. Ceci nous permet de construire un graphe, dit graphe de dépendance approxime, et nous pouvons montrer qu'un critère syntaxique sur ce graphe suffit à montrer la terminaison de tout terme bien typé / The present manuscript is a reflection on termination of higher-order rewrite systems. We concentrate our efforts on a particular approach, size-based termination. This method uses typing to give a syntactic approximation to the size of an element of the language. Our contribution is twofold: first we give a structured approach to proving the correctness of size-based termination. To do this, we show that it is possible to apply a certain version of semantic labelling. This technique uses annotations on terms computed using the semantics of subterms in a certain equational premodel. We show correctness of our labelling framework and of the criterion that allows us to prove termination of the labelled system, and we build a premodel of the rewrite system that intuitively corresponds to the rewrite system. We show that the system labelled using these semantics passes the termination criterion. Furthermore we show that a modification of the classical size-types approach allows us to perform a fine control-flow analysis in a higher-order language. This allows us to build an approximated dependency graph, and show that if a certain syntactic criterion issatisfied by the graph, then all well-typed terms are terminating

Concevoir et mettre en oeuvre des méthodes pour la spécification, l'analyse et la vérification de logiciels et de systèmes sont les principaux moteurs des activités de recherche présentées dans ce manuscrit. Dans ce cadre, nos travaux se positionnent dans la catégorie dite des méthodes formelles appartenant à la communauté plus large du génie logiciel. A l'interface des travaux théoriques et applicatifs, notre objectif est de contribuer aux méthodes permettant d'assurer la correction et la sûreté des systèmes (fonctionnalité, sécurité, fiabilité, ...) en développant ou en améliorant des langages de spécification, des techniques et des outils permettant leur analyse formelle. Dans ce but, nous nous sommes attaché dans cette thèse à proposer et à étudier un cadre formel permettant la définition de politiques de sécurité et la vérification de leurs propriétés. A cet effet, nous avons proposé un cadre pour la spécification de politiques de sécurité basé sur une approche modulaire dans laquelle une politique est vue comme la composition d'un modèle de sécurité et d'une configuration. Nous avons investigué les possibilités offertes par de telles spécifications lorsque les modèles sont exprimés au moyen de contraintes du premier ordre et les configurations au moyen de programmes logiques. En particulier, nous avons proposé un algorithme permettant de transformer une politique exprimée dans un modèle donné vers une autre politique équivalente (au sens où elle engendre les mêmes autorisations) exprimée dans un autre modèle. Dans un second temps, nous nous sommes proposé de tenir compte des aspects dynamiques de la configuration d'une politique vue comme un état du système sur lequel la politique est mise en oeuvre et où chaque action est associée à une procédure de modification des états. Nous avons proposé un langage formel simple pour spécifier séparément les systèmes et les politiques de sécurité puis avons donné une sémantique des spécifications exprimées dans ce cadre sous la forme de systèmes de réécriture. Nous nous sommes ensuite attachés à montrer que les systèmes de réécriture obtenus permettent l'étude de propriétés de sécurité. Dans une troisième partie, nous nous sommes focalisé sur les mécanismes permettant la mise en oeuvre de politiques de sécurité dans les réseaux. Dans ce cadre, nous avons proposé une spécification des firewalls et de leurs compositions basée sur les automates d'arbres et les systèmes de réécriture puis avons montré en quoi ces spécifications nous permettent d'analyser de façon automatique les politiques de sécurité sous-jacentes. / Designing and applying formal methods for specifying, analyzing and verifying softwares and systems are the main driving forces behind the work presented in this manuscript. In this context, our activities fall into the category of formal methods belonging to the wider community of software engineering. At the interface between theoretical and applied research, our aim is to contribute to the methods ensuring the correction and the safety of systems (security, reliability, ...) by developing or by improving specification languages, techniques and tools allowing their formal analysis. In this purpose, we became attached in this thesis to propose and to study a formal framework allowing the specification of security policies and the verification of their properties. We first proposed a framework for specifying security policies based on a modular approach in which policies are seen as a composition of security models and configurations. We investigated the possibilities opened by such specifications when models are expressed by means of first order constraints and configurations by means of logical programs. In particular, we proposed an algorithm allowing the transformation of a security policy expressed in a given model towards another equivalent policy expressed in another model. Secondly, we suggested taking into account dynamic aspects of policy configurations which can be seen as states of the system on which the policy is applied and where each action is associated with a procedure of states modification. We proposed a simple formal language to specify separately systems and security policies and then gave a semantics of specifications expressed in this framework under the form of rewriting systems. We then attempted to show that the obtained rewriting systems allow the analysis of security properties. In the third part, we focused on mechanisms enforcing security policies in networks. In this context, we proposed a specification of firewalls and their compositions based on tree automata and rewriting systems and then showed how these specifications allow us to analyze in an automatic way the underlying security policies.

Cette thèse propose et étudie de nouveaux systèmes déductifs mêlant calculs et déductions. La déduction modulo est un premier formalisme qui traduit un pouvoir calculatoire grâce à un système de réécriture. Nous présentons un paradigme dual appelé superdéduction qui traduit un pouvoir déductif par de nouvelles inférences. Ces pouvoirs calculatoires et déductifs modifient la représentation des preuves et leur interaction par les processus d'élimination des coupures. La normalisation forte ou l'admissibilité des coupures ne sont plus garanties et apparaissent alors comme des propriétés intrinsèques des théories représentées sous forme de systèmes de réécriture. Nous démontrons que certains critères permettent d'assurer ces propriétés, notamment en définissant un langage de termes de preuve pour la superdéduction et en étudiant la permutabilité des inférences en calcul des séquents classique. Notre attention est focalisée sur les calculs des séquents classiques et la représentation des preuves dans de tels systèmes. D'autres formalismes connexes sont envisagés, notamment les réseaux de preuve et le focusing. Nous comparons cette dernière approche à la superdéduction, ce qui nous amène à proposer une refonte du paradigme de superdéduction basée sur un système de multifocusing pour la logique classique. Nous en montrons les effets bénéfiques en démontrant la complétude des systèmes déductifs obtenus. / In this thesis we propose and study several deduction systems that mix deduction and computation. Deduction modulo proposes to translate a computational power through a rewriting system. We present the dual concept called superdeduction. It translates a deductive power into custom inference rules that enrich the deduction system. These computational and deductive powers modify the representation of proofs as well as their interaction through cut-elimination processes. Strong normalisation or cut-admissibility may be lost and therefore appear as intrinsic properties of theories represented as rewriting systems. We prove that certain criteria imply these properties by defining a proof-term language for superdeduction and by studying the permutability of inferences in classical sequent calculus. Our attention is focused on classical sequent calculi and on the representation of proofs in such systems. Other related paradigms are considered, namely proof-nets and focusing. We compare this latter approach with superdeduction. We consequently reforge the superdeduction paradigm on top of a multifocusing system for classical logic. We demonstrate the benefits of this approach by proving the completeness of the obtained deduction systems.

Le processus de développement logiciel est composé d'un grand nombre d'étapes qui intègrent de plus en plus d'outils. Les chaînes de développement de systèmes critiques (aéronautique, domaine médical) font appel à des outils de génération de code basés sur des modèles. Cette complexification a des conséquences sur la vérification des logiciels critiques. Les contraintes légales imposant qu'ils soient certifiés, la qualification des outils utilisés lors de leur développement est nécessaire. Dans cette thèse, nous nous proposons d'aider le processus de qualification en élaborant des méthodes et outils pour le développement fiable. Pour ce faire, nous présentons une méthode hybride de transformation de modèles par réécriture. Nous nous appuyons sur le langage Tom qui fournit de nouvelles fonctionnalités aux langages généralistes par l'ajout de constructions dédiées. Nous proposons aussi une traçabilité de ces transformations afin de répondre aux exigences de la qualification. La trace générée peut être utilisée a posteriori à des fins de vérification. / Software development process is composed of steps which integrate an increasing number of tools. Development chains for critical systems (avionics, health field) have gradually adopted model-based code generation tools. This increase of complexity has consequences on critical software verification. As legal constraints require to certify them, tools used during the development have to be qualified. In this thesis, we propose to help the qualification process by providing methods and tools for liable development. To do so, we present an hybrid models transformation method based on rewriting. We rely upon Tom language which provides new features to general purposes languages by adding dedicated constructs. We also propose a traceability in order to respect qualification requirements. The generated trace can then be used for verification purpose

Made available in DSpace on 2016-03-22T17:26:20Z (GMT). No. of bitstreams: 1 Ana Viana.pdf: 774568 bytes, checksum: 527b7abc65250c7237f786bc2b21c6c0 (MD5) Previous issue date: 2004-07-30 / Les stéréotypes de féminin et de masculin présents dans les contes de fées traditionels sont institués em tant qu étant, au dela de différents, opposés. Cette doublé vision de l indentité de genre s institue dans le imaginaire, produisant des discours sexiste et perpétuant des pratiques sociales reconnues comme différentes, dichotomiques. Dans cette étude, je me propose à rechercher s il est possible que la réécriture du conte de fées reflete le processus de (re)signification de la dualité féminin/masculin et comment cela se passe. Je pense que le functionnement discursif de ce type de texte pourrait bien être em renversant et même em trasformant ces pratiques sociales, une fois qu il se constitue dans um espace de (re)signification de modèles de rapports sociaux et de rapports de pouvoir lequels sont institués à partir de nouvelles et différentes positions-sujets. Le corpus empirique de cette recherche est composé par la chronique Psiu , de Luis Fernando Veríssimo, laquelle contient sept réécritures du conte traditionnel Le Roi Crapaud, dês Fréres Grimm. Pour baser l analyse, j emploie le référentiel théorique de l Analyse de Discours d orientation française et de la Théorie Critique Féministe / Os estereótipos de feminino e de masculino presentes nos contos de fadas tradicionais, instituem-se como sendo, além de diferentes, contrapostos. Essa dupla visão da identidade de gênero instaura-se no imaginário, gerando discursos sexistas e perpetuando práticas sociais reconhecidas como diferentes, dicotômicas. Busco, neste estudo, investigar como e se a reescritura dos contos de fadas estaria refletindo o processo de (re)significação da dualidade feminino/masculino. Acredito que o funcionamento discursivo desse tipo de texto poderá estar subvertendo e até mesmo transformando essas práticas sociais, uma vez que se constitui em um espaço de (re)significação de modelos de relações sociais e relações de poder que são instituídas a partir de novas e diferentes posições-sujeito. O corpus empírico desta investigação é composto pela crônica Psiu, de Luis Fernando Veríssimo, que por sua vez, contém sete reescrituras do conto tradicional O rei sapo, dos Irmãos Grimm. Para fundamentar a análise, utilizo o referencial teórico da Análise de Discurso de linha francesa e da Teoria Crítica Feminista

L’objectif de cette recherche est une étude globale de l’œuvre et de la pensée de l’humaniste milanais Ortensio Lando (1506 env.- 1553 env.). Cet auteur, redécouvert par la critique dans les années 70, notamment grâce aux recherches menées par les américains Conor Fahy et Paul Grendler, connaît aujourd’hui un intérêt renouvelé en raison du caractère paradoxal et ambigu de sa production. Mais, si son ouvrage le plus célèbre, les Paradossi (1543), est désormais bien connu par les spécialistes, la plus grande partie de ses écrits reste encore méconnue. Nous prendrons par conséquent en considération tout le corpus de Lando, qui compte au moins une vingtaine d’ouvrages, pour mener une étude complète de son œuvre.Nous porterons aussi une attention particulière à la vie d’Ortensio Lando qui reste encore en grande partie obscure. Nous reprendrons les quelques documents de l’époque qui nous donnent des informations utiles et les différentes théories sur la biographie de Lando, notamment l’hypothèse qu’il était dans sa jeunesse un moine augustin qui aurait par la suite abandonné son ordre pour fuir en France.L’analyse des œuvres permet de dégager trois axes principaux :1) L’autopromotion.Lando employait différents pseudonymes. À notre avis, cet usage était dicté seulement en partie par la nécessité de cacher son identité d’auteur hétérodoxe. L’utilisation de pseudonymes et de jeux linguistiques faisait aussi partie d’une stratégie réfléchie d’autopromotion dont nous analyserons les techniques rhétoriques. Lando était conscient des nouveaux enjeux de l’industrie typographique et démontre qu’il sait les utiliser à sa faveur pour se construire une image de lettré irrégulier et excentrique.2) Le paradoxe.Les Paradossi sont considérés comme la première œuvre du genre paradoxal en langue vulgaire, genre qui connaîtra un énorme succès pendant tout le XVIe siècle. La critique a déjà reconstruit la façon dont l’humanisme a récupéré cette tradition d’origine antique, notamment à travers Lucien de Samosate, elle en a isolé les thématiques principales comme celle "asinienne" et la critique du savoir. Jusqu’à présent, peu d’attention a été accordée aux autres textes paradoxaux de Lando et il manque encore une interprétation satisfaisante des raisons qui se cachent derrière cette stratégie stylistique. Les théories qui considèrent Ortensio Lando comme un antihumaniste, anticicéronien et antiérasmien ne sont pas complètement convaincantes et nous développerons une autre thèse pour expliquer l’emploi du paradoxe : l’ambiguïté du message ne représente ni un refus sceptique de toute position, ni une prise de position contre l’héritage humaniste mais le rejet de toute forme de dogmatisme intellectuel.3) Les formes de réécriture.Si Lando ne peut pas être considéré comme antihumaniste, il est certain que nous nous trouvons dans une période de crise et de changement des modèles littéraires. La problématique sera donc d’analyser quels sont les rapports de Lando avec la culture classique dont il reprend et parodie les genres, et avec la culture humaniste qui bien que critiquée reste au centre de ses œuvres. Nous nous concentrerons aussi sur les raisons qui se cachent derrière l’emploi de longues catalogues d’exemples érudits, tirés surtout de l’Officina de Jean Tixier, en proposant de lier cette pratique à une parodie des dérives de la récupération du savoir classique, se fondant sur les mêmes prémisses de littérature paradoxale. / The aim of this study is to analyse the work and thought of Italian humanist Ortensio Lando (c. 1506 – c. 1553). This writer has been rediscovered by critics in the 1970s, mostly thanks to Fay’s and Grendler’s studies, and today many researchers are interested by paradox and ambiguity in his works. But, except for the Paradossi, his literary production remains mostly unknown. For this reason we considered the whole Lando’s corpus, about 27 works, in order to propose a monographic study of this writer.We also focused on Ortensio Lando’s biography, of which we have only few documents, and on the theory that he was an Augustinian monk who committed apostasy and fled to France.The analysis of Lando’s works has permitted to define three research axes:1) Self-promotionLando used different pseudonyms. We assume that this strategy was not only a way to cover his identity, but also a self-promotion stratagem of which we analysed the rhetorical function. Lando knew how to exploit printing innovations and he showed how they could be used to build his eccentric writer’s image.2) ParadoxThe Paradossi are considered as the first vernacular paradoxical work, a successful literary genre in 16th century. Literary criticism reconstructed the way paradoxical tradition was reworked by Humanism, especially through Lucian of Samosata, and has defined its main issues, like the “donkey’s praise” and the critical of learning. But so far, little consideration has been given to others paradoxical Lando’s works and there’s still no satisfying interpretation of the reason behind this strategy. Several assumptions considered Lando as an anti-humanist, anti-Ciceronian and anti-Erasmian writer, but we believe that paradox doesn’t carries a sceptical rejection of any opinion or a criticism against Humanistic heritage; paradox is rather a denunciation of intellectual dogmatism.3) RewritingEven if Lando cannot be considered as an anti-humanist, he clearly lived in times of intellectual crisis and paradigmatic shift in literary models. We will analyse the relationship between Lando and classical culture by parody and imitation, and the relationship between the writer and humanistic culture that remains, despite criticism, the focus of his work. We will also focus on the reasons behind the long and erudite catalogues that Lando copies, especially from Ravisius’s Officina, by proposing to link this practice to the parody of uncritical classical imitation, as in the case of paradoxical literature.