Les systèmes multi-agents (SMA) peuvent être utilisé pour modéliser les phénomènes qui peuvent être décomposés en agents qui interagissent et qui existent au sein d'un environnement. Ils peuvent être utilisés pour modéliser les sociétés humaines et animales, aux fins de l'analyse de leurs propriétés par des moyens de calcul. Cette thèse est consacrée à l'analyse automatisée d'un type particulier de ces modèles sociaux, celles qui sont fondées sur les principes comportementalistes, qui contrastent avec les approches cognitives plus dominantes dans la littérature des SMAs. La caractéristique des théories comportementalistes est l'accent mis sur la définition des comportements basée sur l'interaction entre les agents et leur environnement. Non seulement des actions réflexives, mais aussi d'apprentissage, les motivations, et les émotions peuvent être définies. Nous introduisons une architecture formelle d'agent basée sur la théorie d'analyse comportementale de B. F. Skinner, ainsi que une notion appropriée et formelle de l'environnement pour mettre ces agents ensemble dans un SMA. La simulation est souvent utilisée pour analyser les SMAs. Les techniques consistent généralement à simuler le SMA plusieurs fois, soit pour recueillir des statistiques, soit pour voir ce qui se passe à travers l'animation. Toutefois, les simulations peuvent être utilisées d'une manière plus orientée vers la vérification si on considère qu'elles sont en réalité des explorations de grandes espaces d'états. Nous proposons une technique de vérification nouvelle basé sur cette idée, qui consiste à simuler un SMA de manière guidée, afin de vérifier si quelques hypothèses sur lui sont confirmées ou non. À cette fin, nous tirons profit de la position privilégiée que les environnements sont dans les SMAs de cette thèse: la spécification formelle de l'environnement d'un SMA sert à calculer les évolutions possibles du SMA comme un système de transition, établissant ainsi l'espace d'états à vérifier. Dans ce calcul, les agents sont pris en compte en les simulant afin de déterminer, à chaque état de l'environnement, quelles sont leurs actions. Chaque exécution de la simulation est une séquence d'états dans cet espace d'états, qui est calculée à la volée, au fur et à mesure que la simulation progresse. L'hypothèse à étudier, à son tour, est donnée comme un autre système de transition, appelé objectif de simulation, qui définit les simulations désirables et indésirables. Il est alors possible de vérifier si le SMA est conforme à l'objectif de simulation selon un certain nombre de notions de satisfiabilité très précises. Algorithmiquement, cela correspond à la construction d'un produit synchrone de ces deux systèmes de transitions (i.e., celui du SMA et l'objectif de simulation) à la volée et à l'utiliser pour faire fonctionner un simulateur. C'est-à-dire, l'objectif de simulation est utilisé pour guider le simulateur, de sorte que seuls les états concernés sont en réalité simulés. À la fin d'un tel algorithme, il délivre un verdict concluant ou non concluant. Si c'est concluant, il est connu que le SMA est conforme à l'objectif de simulation par rapport aux observations qui ont été faites lors des simulations. Si c'est non-concluant, il est possible d'effectuer quelques ajustements et essayer à nouveau. En résumé, dans cette thèse nous fournissons quatre nouveaux éléments: (i) une architecture d'agent; (ii) une spécification formelle de l'environnement de ces agents, afin qu'ils puissent être composés comme un SMA; (iii) une structure pour décrire les propriétés d'intérêt, que nous avons nommée objectif de simulation, et (iv) une technique pour l'analyse formelle du SMA résultant par rapport à un objectif de simulation. Ces éléments sont mis en œuvre dans un outil, appelé Simulateur Formellement Guidé (FGS, de l'anglais Formally Guided Simulator).Des études de cas exécutables dans FGS sont fournies pour illustrer l'approche. / Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely reflexive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as a MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., "every time the agent does X, it will do Y later"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS's and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose w.r.t. the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again.In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into a MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach.

Ce travail appartient au domaine de la simulation numérique sur des plates-formes d'exécution distribuées hétérogènes telles que des grilles de calcul. Ce type de plate-forme se caractérise par des possibles changements de condition d'exécution et par une probabilité importante de défaillance de certains composants. Une application qui s'exécute dans un tel environnement se doit d'être adaptable à son contexte d'exécution et tolérante aux pannes. Face à la complexité croissante de la mise en place de cas de calcul sur des grilles de calcul, nous proposons une plateforme logicielle pour la résolution de cas de calcul numérique dans un environnement distribué hétérogène. Nos travaux apportent une solution qui se base sur un système d'agents mobiles, ce qui permet à une application de s'adapter au changement de son environnement d'exécution. Dans un premier temps, nous utilisons le langage pi calcul d'ordre supérieur pour spécifier une « ferme de travailleurs » capable de participer à la résolution de tout type de cas de calcul. Ensuite, nous énonçons des propriétés qui caractérisent le bon fonctionnement de ce système avec une logique temporelle TCTL. Pour cela, nous souhaitons modéliser notre système à l'aide d'automates temporisés à partir des termes définis par la spécification formelle en pi calcul. Dans ce but, nous définissons une transformation de termes écrits en pi calcul en automates temporisés. Les propriétés sont alors vérifiées avec l'outil UppAal. Pour valider ce travail de modélisation, nous avons réalisé le framework MCA (pour Mobile Computing Architecture). Celui-ci propose un ensemble d'outils facilitant la mise en place de composants sur un environnement distribué hétérogène dans le but d'effectuer la résolution de cas de calcul. La librairie avec laquelle sont développés ces composants, qu'ils soient mobiles ou non, est implantée en Java et se base les technologies Jini et JavaSpaces. Enfin, nous réalisons l'évaluation du framework MCA en procédant à la résolution de trois cas de calcul différents. Chacune de ces expériences, réalisées sur une grappe de 20 noeuds, nous permet de montrer les caractéristiques essentielles de notre framework : une simplicité de programmation, un faible surcoût en temps d'exécution sans l'activation de la tolérance aux pannes et une tolérance aux pannes efficace / This work belongs to the domain of numerical simulation on heterogeneous distributed platforms such as grids. This type of platform is characterized by possible changes in execution conditions and a significant probability of some components failure. An application running in such an environment must be adaptable to its execution context and fault tolerant. Facing the growing complexity of implementing computation cases on grid computing, we propose a software platform which solves numerical computation cases in a distributed heterogeneous environment. Our work provides a solution based on a mobile agent system, which allows an application to adapt to change in its execution environment. At first, we use the higher-order pi calculus language to specify a « farm of workers » able to take part in solving any type of computation case. Then we set the properties that characterize the system's correct execution with a temporal logic TCTL. In order to do this, we perform a temporal modeling system based on terms defined by the formal specification in pi calculus. To achieve this transformation, we define a translation of terms written in pi calculus into timed automata. The properties are verified with the UppAal tool. To validate this modeling work, we develop the MCA (for Mobile Computing Architecture) framework. It offers a set of tools which facilitate the implementation of distributed heterogeneous components in order to solve computation cases. These components, mobile or not, are developed with a library written in Java and which uses Jini and JavaSpaces technologies. Finally, our framework is evaluated through the resolution of three different computation cases. Each of these experiments, performed on a 20 node cluster allow us to highlight our framework's main characteristics : programming simplicity, low overhead in execution time without the fault tolerance activation and efficient fault tolerance

Cette thèse est composée d'une partie sur la conjecture des familles stables par unions et de quatre autres chapitres consacrés aux sujets liés aux suites automatiques. Dans la première partie, on donne une condition suffisante pour qu'une version affaiblie de la conjecture soit vraie. On donne aussi un majorant de la fréquence maximale minimale dans une famille de taille $n$. Dans Chapitre 3 on démontre que la formule d'extraction des coefficients des séries algébriques connue pour les corps à caractéristique $0$ est une conséquence d'un théorème de Furstenberg qui permet d'écrire certaines séries algébriques comme les diagonales des fractions rationnelles à deux variables. Comme ce théorème est valide pour tous les corps, la formule l'est aussi. Dans Chapitre 4 on donne une généralisation des résultats de J.-P. Allouche et J. Shallit concernant certains produits infinis et les fonctions qui comptent le nombre d'occurrences d'un facteur dans l'expansion en base $B$ de $n$. Dans Chapitre 5 on donne une construction explicite d'un mot infini avec complexité en facteur de $\Theta(n^t)$ avec la valuation $p$-adique. Dans Chapitre 6 on donne une nouvelle démonstration de la transcendance de la série formelle $L(1,\chi_s)/\Pi$, où $L$ est un analogue des fonctions $L$ de Dirichlet en caractéristique finie défini par D. Goss et $\Pi$ l'analogue de $\pi$ défini par L. Carlitz. / This thesis comprises one part concerning the union-closed sets conjecture and four other chapters dedicated to subjects related to automatic sequences. In the first part, we give a sufficient condition for a weaker version of the conjecture ($\varepsilon$-union closed sets conjecture) to hold. We also give an upper bound of the minimal maximal frequency for a family of size $n$. In Chapter 3 we prove that the coefficient extraction formula for algebraic series known for fields of characteristic $0$ is a consequence of a theorem of Furstenberg that says certains algebraic series can be written as the diagonals of a rational fractions in two variables. As the theorem is true for all fields, so is the formula. In Chapter 4 we give a generalization of the result of J.-P. Allouche and J. Shallit concerning certain infinite products and block-counting functions. In Chapter 5 we give an explicit construction based on $p$-adic valuation of an infinite word with subword complexity $\Theta(n^t)$. In Chapter 6 we give a new proof of the transcendence of the power series $L(1,\chi_s)/\Pi$, where $L$ is an analogue in positive characteristics of Dirichlet $L$ functions defined by D. Goss and $\Pi$ the analogue of $\pi$ defined by L. Carlitz.

Cette thèse présente une formalisation en Coq des langages et des algorithmes fondamentaux portant sur les bases de données. Ainsi, ce fourni des spécifications formelles issues des deux approches différentes pour la définition des modèles de données: une basée sur l’algèbre et l'autre basée sur la logique.A ce titre, une première contribution de cette thèse est le développement d'une bibliothèque Coq pour le modèle relationnel. Cette bibliothèque contient les modélisations de l’algèbre relationnelle et des requêtes conjonctives. Il contient aussi une mécanisation des contraintes d'intégrité et de leurs procédures d'inférence. Nous modélisons deux types de contraintes: les dépendances, qui sont parmi les plus courantes: les dépendances fonctionnelles et les dépendances multivaluées, ainsi que leurs axiomatisations correspondantes. Nous prouvons formellement la correction de leurs algorithmes d'inférence et, pour le cas de dépendances fonctionnelles, aussi la complétude.Ces types de dépendances sont des instances de contraintes plus générales : les dépendances génératrices d'égalité (equality generating dependencies, EGD) et, respectivement, les dépendances génératrices de tuples (tuple generating dependencies, TGD), qui appartiennent a une classe encore plus large des dépendances générales (general dependencies). Nous modélisons ces dernières et leur procédure d'inférence, i.e, "the chase", pour lequel nous établissons la correction. Enfin, on prouve formellement les théorèmes principaux des bases de données, c'est-à-dire, les équivalences algébriques, la théorème de l' homomorphisme et la minimisation des requêtes conjonctives.Une deuxième contribution consiste dans le développement d'une bibliothèque Coq/ssreflect pour la programmation logique, restreinte au cas du Datalog. Dans le cadre de ce travail, nous donnons la première mécanisations d'un moteur Datalog standard et de son extension avec la négation. La bibliothèque comprend une formalisation de leur sémantique en theorie des modelés ainsi que de leur sémantique par point fixe, implémentée par une procédure d'évaluation stratifiée. La bibliothèque est complétée par les preuves de correction, de terminaison et de complétude correspondantes. Cette plateforme ouvre la voie a la certification d' applications centrées données. / This thesis presents a formalization of fundamental database theories and algorithms. This furthers the maturing state of the art in formal specification development in the database field, with contributions stemming from two foundational approches to database models: relational and logic based.As such, a first contribution is a Coq library for the relational model. This contains a mechanization of integrity constraints and of their inference procedures. We model two of the most common dependencies, namely functional and multivalued, together with their corresponding axiomatizations. We prove soundness of their inference algorithms and, for the case of functional ones, also completeness. These types of dependencies are instances of equality and, respectively, tuple generating dependencies, which fall under the yet wider class of general dependencies. We model these and their inference procedure,i.e, the chase, for which we establish soundness.A second contribution consists of a Coq/Ssreflect library for logic programming in the Datalog setting. As part of this work, we give (one of the) first mechanizations of the standard Datalog language and of its extension with negation. The library includes a formalization of their model theoretical semantics and of their fixpoint semantics, implemented through bottom-up and, respectively, through stratified evaluation procedures. This is complete with the corresponding soundness, termination and completeness proofs. In this context, we also construct a preliminary framework for dealing with stratified programs. This work paves the way towards the certification of data-centric applications.

Au sein de la communauté scientifique, l’étude des réseaux d’énergie suscite un vif intérêt puisque ces infrastructures deviennent de plus en plus importantes dans notre monde moderne. Des outils mathématiques avancés et complexes sont nécessaires afin de bien concevoir et mettre en œuvre ces réseaux. La précision et l’optimalité sont deux caractéristiques essentielles pour leur conception. Bien que ces deux aspects soient au cœur des méthodes formelles, leur application effective reste largement inexplorée aux réseaux d’énergie. Cela motive fortement le travail développé dans cette thèse. Un accent particulier est placé sur le problème général de planification de la consommation d'énergie. Il s'agit d'un scénario dans lequel les consommateurs ont besoin d’une certaine quantité d’énergie et souhaitent que cette demande soit satisfaite dans une période spécifique (e.g., un Véhicule Électrique (VE) doit être rechargé dans une fenêtre de temps définie par son propriétaire). Par conséquent, chaque consommateur doit choisir une puissance de consommation à chaque instant (par un système informatisé), afin que l'énergie finale accumulée atteigne un niveau souhaité. La manière dont les puissances sont choisies est obtenue par l’application d’une « stratégie » qui prend en compte à chaque instant les informations pertinentes d'un consommateur afin de choisir un niveau de consommation approprié (e.g., l’énergie accumulée pour recharge le VE). Les stratégies peuvent être conçues selon une approche centralisée (dans laquelle il n'y a qu'un seul décideur qui contrôle toutes les stratégies des consommateurs) ou décentralisée (dans laquelle il y a plusieurs contrôleurs, chacun représentant un consommateur). Nous analysons ces deux scénarios dans cette thèse en utilisant des méthodes formelles, la théorie des jeux et l’optimisation. Plus précisément, nous modélisons le problème de planification de la consommation d'énergie à l'aide des processus de décision de Markov et des jeux stochastiques. Par exemple, l’environnement du système électrique, à savoir : la partie non contrôlable de la consommation totale (e.g., la consommation hors VEs), peut être représentée par un modèle stochastique. La partie contrôlable de la consommation totale peut s’adapter aux contraintes du réseau de distribution (e.g., pour ne pas dépasser la température maximale d'arrêt du transformateur électrique) et à leurs objectifs (e.g., tous les VEs soient rechargés). Cela peut être vu comme un système stochastique avec des multi-objectifs sous contraintes. Par conséquent, cette thèse concerne également une contribution aux modèles avec des objectives multicritères, ce qui permet de poursuivre plusieurs objectifs à la fois et une conception des stratégies qui sont fonctionnellement correctes et robustes aux changements de l'environnement. / Within the research community, there is a great interest in exploring many applications of energy grids since these become more and more important in our modern world. To properly design and implement these networks, advanced and complex mathematical tools are necessary. Two key features for their design are correctness and optimality. While these last two properties are in the core of formal methods, their effective application to energy networks remains largely unexploited. This constitutes one strong motivation for the work developed in this thesis. A special emphasis is made on the generic problem of scheduling power consumption. This is a scenario in which the consumers have a certain energy demand and want to have this demand fulfilled before a set deadline (e.g., an Electric Vehicle (EV) has to be recharged within a given time window set by the EV owner). Therefore, each consumer has to choose at each time the consumption power (by a computerized system) so that the final accumulated energy reaches a desired level. The way in which the power levels are chosen is according to a ``strategy’’ mapping at any time the relevant information of a consumer (e.g., the current accumulated energy for EV-charging) to a suitable power consumption level. The design of such strategies may be either centralized (in which there is a single decision-maker controlling all strategies of consumers), or decentralized (in which there are several decision-makers, each of them representing a consumer). We analyze both scenarios by exploiting ideas originating from formal methods, game theory and optimization. More specifically, the power consumption scheduling problem can be modelled using Markov decision processes and stochastic games. For instance, probabilities provide a way to model the environment of the electrical system, namely: the noncontrollable part of the total consumption (e.g., the non-EV consumption). The controllable consumption can be adapted to the constraints of the distribution network (e.g., to the maximum shutdown temperature of the electrical transformer), and to their objectives (e.g., all EVs are recharged). At first glance, this can be seen as a stochastic system with multi-constraints objectives. Therefore, the contributions of this thesis also concern the area of multi-criteria objective models, which allows one to pursue several objectives at a time such as having strategy designs functionally correct and robust against changes of the environment.

Dans le but de faciliter la tâche d'évaluation du niveau de sécurité incendie aux ingénieurs et permettre aux spécialistes impliqués dans le domaine d'utiliser leurs langages et outils préférés, nous proposons de créer un langage dédié au domaine de la sécurité incendie générant automatiquement une simulation en prenant en considération les langages métiers utilisés par les spécialistes intervenants dans le domaine. Ce DSL nécessite la définition, la formalisation, la composition et l'intégration de plusieurs modèles, par rapport aux langages spécifiques utilisés par les spécialistes impliqués dans le domaine. Le langage spécifique dédié au domaine de la sécurité incendie est conçu par composition et intégration de plusieurs autres DSLs décrits par des langages techniques et naturels (ainsi que des langages naturels faisant référence à des langages techniques). Ces derniers sont modélisés de manière à ce que leurs composants soient précis et fondés sur des bases mathématiques permettant de vérifier la cohérence du système (personnes et matériaux sont en sécurité) avant sa mise en œuvre. Dans ce contexte, nous proposons d'adopter une approche formelle, basée sur des spécifications algébriques, pour formaliser les langages utilisés par les spécialistes impliqués dans le système de génération, en se concentrant à la fois sur les syntaxes et les sémantiques des langages dédiés. Dans l'approche algébrique, les concepts du domaine sont abstraits par des types de données et les relations entre eux. La sémantique des langages spécifiques est décrite par les relations, le mapping (correspondances) entre les types de données définis et leurs propriétés. Le langage de simulation est basé sur un langage conçu par la composition de plusieurs DSL spécifiques précédemment décrits et formalisés. Les différents DSLs sont implémentés en se basant sur les concepts de la programmation fonctionnelle et le langage fonctionnel Haskell bien adapté à cette approche. Le résultat de ce travail est un outil informatique dédié à la génération automatique de simulation, dans le but de faciliter la tâche d'évaluation du niveau de sécurité incendie aux ingénieurs. Cet outil est la propriété du Centre Scientifique et Technique du bâtiment (CSTB), une organisation dont la mission est de garantir la qualité et la sécurité des bâtiments, en réunissant des compétences multidisciplinaires pour développer et partager des connaissances scientifiques et techniques, afin de fournir aux différents acteurs les réponses attendues dans leur pratique professionnelle. / In order to facilitate the engineers task of evaluating the fire safety level, and to allow the specialists involved in the field to use their preferred languages and tools, we propose to create a language dedicated to the field of fire safety, which automatically generates a simulation, taking into account the specific languages used by the specialists involved in the field. This DSL requires the definition, the formalization, the composition and the integration of several models, regardig to the specific languages used by the specialists involved in the field. The specific language dedicated to the field of fire safety is designed by composing and integrating several other DSLs described by technical and natural languages (as well as natural languages referring to technical ones). These latter are modeled in a way that their components must be precise and based on mathematical foundations, in order to verify the consistency of the system (people and materials are safe) before it implementation. In this context, we propose to adopt a formal approach, based on algebraic specifications, to formalize the languages used by the specialists involved in the generation system, focusing on both syntaxes and semantics of the dedicated languages. In the algebraic approach, the concepts of the domain are abstracted by data types and the relationships between them. The semantics of specific languages is described by the relationships, the mappings between the defined data types and their properties. The simulation language is based on a composition of several specific DSLs previously described and formalized. The DSLs are implemented based on the concepts of functional programming and the Haskell functional language, well adapted to this approach. The result of this work is a software dedicated to the automatic generation of a simulation, in order to facilitate the evaluation of the fire safety level to the engineers. This tool is the property of the Scientific and Technical Center for Building (CSTB), an organization whose mission is to guarantee the quality and safety of buildings by combining multidisciplinary skills to develop and share scientific and technical knowledge, in order to provide to the different actors the expected answers in their professional practice.

Bien qu’une vaste littérature musicologique porte sur Joseph Haydn (1732-1809), aucune ne comprend une étude exhaustive de l’ensemble de ses sonates pour clavier, incluant les premières oeuvres composées dans la décennie 1750. La présente recherche se propose de combler en partie cette lacune par le biais d’une analyse des 52 premiers mouvements Hoboken (Hob.) XVI. Basée sur des outils empruntés principalement à William E. Caplin, Brian Alegant et Don McLean, cette étude constitue un premier pas vers une typologie du premier mouvement de sonate chez Haydn, permettant par le fait même de refléter l’évolution de la forme sonate, en mutation tout au long de la vie créative du compositeur. Dans un premier temps, une série d’analyse capliniennes permet d’effectuer un survol des différentes formes qui composent le corpus à l’étude afin d’en dégager certains procédés spécifiques, nommément l’exploitation de techniques formelles à des fins de développement thématique, ainsi que l’emploi marqué d’ambiguïtés formelles et fonctionnelles. Dans un second temps, une analyse de la disposition du matériau suggère une conception du premier mouvement en forme sonate basée sur le développement thématique d’un nombre réduit d’idées musicales, dont la répétition est compensée par plusieurs procédés dont les principaux sont la variation structurelle dans la section de réexposition et l’emploi de différentes fonctions formelles à chaque itération. Prises dans leur ensemble, ces analyses démontrent que l’ensemble des premiers mouvements de sonate pour clavier Hob. XVI sont liées par une certaine imprévisibilité créée spécifiquement au moyen de la réutilisation thématique et des fonctions formelles. / Although there is a vast musicological literature on Joseph Haydn (1732-1809), none includes an exhaustive study of all his keyboard sonatas, including the first works composed in the 1750s. The present research aims to fill this gap through an analysis of the 52 first movements of the keyboard sonatas Hoboken (Hob.) XVI. This study constitutes a first step towards a typology of Haydn’s sonata first movement, thereby making it possible to look at the evolution of the sonata form, under development throughout the composer's creative life. Initially, a first series of Caplinian analysis allows an overview of the different forms that make up the corpus under study in order to identify certain specific procedures, namely the use of formal techniques for thematic development purposes as well as the marked use of formal and functional ambiguities. Secondly, an analysis of the arrangement of the material suggests the conception of the sonata form’s first movement to be based on the thematic development of a reduced number of ideas, the repetition of which is compensated for by several processes, the main ones of which are structural variation in the recapitulation section as well as the use of various formal functions for each iteration. Taken as a whole, these analysis show that the 52 first movements Hob. XVI are linked by the expression of a certain unpredictability caused specifically by thematic restatement and the use of various formal functions.

La représentation de phénomènes naturels fait partie des domaines les plus complexes et les plus actifs de la recherche en informatique graphique. Notre compréhension de la nature s'améliorant au fil des années, les chercheurs ne cessent de proposer des nouveaux modèles, toujours plus pertinents les uns que les autres, et permettant de reproduire les différents phénomènes naturels que nous pouvons observer autour de nous, dans la vie de tous les jours. Nous nous sommes intéressés à la représentation du fruit et des différents éléments qui le caractérisent. Le fruit est un objet complexe et, en fonction de la précision requise, sa conception à l'aide de logiciels de modélisation 3D peut très vite devenir compliquée. Notre modèle permet de générer une grande variété de fruits de formes différentes ainsi que les différents éléments de leur structure interne et ce, grâce à l'utilisation d'une seule grammaire. Au sein d'une même espèce, les fruits générés seront tous différents au niveau de leur forme, tout en restant semblables. La seconde partie de nos travaux porte quant à elle sur la représentation des imperfections géométriques qui sont propres aux fruits. Les fruits sont le résultat de l'enchaînement d'un très grand nombre de processus physiologiques complexes qui interagissent fortement entre eux. Lorsque le bon fonctionnement de l'un de ces processus est compromis, cette anomalie se matérialise sur le fruit par l'apparition de défauts au niveau de sa forme. Notre modèle propose une approche simple, basée sur l'utilisation de grammaires, qui permettent d'altérer soit la forme générale d'un fruit soit des parties de sa surface. / One of the largest areas of research in computer graphics deals with natural phenomena representation. Over the years, as our understanding of nature grew, researchers started to propose new ways of simulating the various natural phenomena that we can observe in our everyday life. In this thesis, we focused on the representation of fruits. The fruit is a complex object. Depending on the desired accuracy, modeling a 3D fruit using classic 3D modeling software can become very tedious. We propose a model for generating vast varieties of fruits as well as their internal structure, thanks to the use of a single formal grammar. Each fruit that will be generated using our method will have global features that characterize its species, but it will also have local variations that are specific to it. The second part of ou work involves the representation of geometrical imperfections along the fruit. The fruit is the result of a series of physiological processes that strongly interact with each other. When one of these processes does not work the way it should, this dysfunction is materialized in the form of a shape defect. Our model introduces a simple approach, based on the use of grammars, which will allow us to apply variations on fruits in order to generate various categories of shape defects.

Le développement de méthodes de synthèse asymétrique est très important pour l’accès à des molécules à visées thérapeutiques. Dans ce contexte, nous nous sommes intéressés à l’utilisation d’organocatalyseurs chiraux pour la synthèse de molécules cycliques énantioenrichies. Dans une première partie sont présentées des réactions de cycloadditions formelles (3+2), (4+2) et (4+3) à partir d’ènecarbamates ou de diènecarbamates catalysées par des acides phosphoriques chiraux. Ces derniers étant bifonctionnel, ils permettent l’activation des deux partenaires de cycloaddition menant à la synthèse d’indolines, de 2,3-dihydrobenzofuranes, de benzoquinones carbonannulées, de cyclohepta[b]indoles et de tétrahydroquinolines de façon hautement stéréosélective. Dans une seconde partie, nous nous sommes intéressés à l’utilisation de composés d’iode hypervalent chiraux comme organocatalyseurs. En effet, ces composés présentent une réactivité intéressante tout en étant stable et faiblement toxique. Ainsi, leur utilisation dans une réaction de lactonisation à partir de substrats flexibles a permis l’obtention de divers hétérocycles avec de bons résultats. / The development of new enantioselective methodologies is essential for the synthesis of bioactive compounds. In this context, we were interested in using organocatalysts for the synthesis of enantioenriched cyclic molecules. In a first part will be describe chiral phosphoric acid catalyzed (3+2), (4+2) and (4+3) formal cycloadditions using enecarbamate or dienecarbamate. These catalysts are bifunctional and can interact with both cycloaddition partners leading to the synthesis of 2,3-dihydrobenzofuranes, carboannulated benzoquinones, cyclohepta[b]indoles and tetrahydroquinolines with high stereocontrol. In a second phase, we were interested in using chiral hypervalent iodine as organocatalyst. Theses compounds present interesting reactivity while being stable and not very toxic. Their use permits us to develop a lactonisation starting from flexible substrate and led to the synthesis of various heterocycles with good results.

Face aux enjeux environnementaux actuels, la catalyse est devenue un outil majeur pour la synthèse de molécules complexes et à visées thérapeutiques. Dans ce contexte, nous nous sommes intéressés au développement de nouvelles méthodes de synthèses innovantes, efficaces, sans métaux ou activées par la lumière visible. Ainsi, mes travaux de thèse ont fait appel à deux thématiques largement étudiées au sein de notre laboratoire que sont la catalyse photorédox et l'organocatalyse. Dans ce manuscrit, la première partie porta sur la conception de réactions multicomposants photocatalysées pour la synthèse de structures trifluorométhylées avec de bons rendements. La partie suivante a été consacrée au développement et à l’évaluation de nouveaux photocatalyseurs supportés, robustes et recyclables. La troisième partie présenta l’élaboration de réactions de cyloadditions formelles (4+3) et (4+2), catalysées aux acides phosphoriques chiraux pour une synthèse efficace, énantiosélective et diastéréosélective de cyclohepta[b]indoles et de spiroindolines. Dans la quatrième partie, une stratégie combinant l’organocatalyse asymétrique et la photocatalyse pour la synthèse de tryptamines α-substituées β-aminées potentiellement biologiquement actives a été décrite. Enfin, l’élaboration de nouveaux composés d’iode hypervalent chiraux et leur évaluation en tant qu’organocatalyseurs fût rapportées dans la dernière partie de ce manuscrit de thèse. / In front of current environmental challenges, catalysis has become a major tool for the synthesis of complex and therapeutic molecules. In this context, we have focused on the development of new synthesis methods that are innovative, efficient, metal-free or activated by visible light. Thus, my thesis work has involved two themes that have been widely studied in our team: photoredox catalysis and organocatalysis. In this manuscript, the first part focused on the conception of photocatalyzed multicomponent reactions for the synthesis of trifluoromethylated structures with good yields. The following section devoted to the design and evaluation of new supported, robust and recyclable photocatalysts. The third part presented the formulation of formal (4+3) and (4+2) cyloaddition reactions, catalyzed with chiral phosphoric acids for an effective, enantio- and diastereo-selective synthesis of cyclohepta[b]indoles and spiroindolines. In the fourth part, a strategy combining asymmetric organocatalysis and photocatalysis for the synthesis of potentially biologically active α-substituted β-amino tryptamines was described. Finally, the elaboration of new chiral hypervalent iodine compounds and their evaluation as organocatalysts was reported in the last part of this thesis manuscript.