Ces dernières années, le domaine des bases de données a beaucoup évolué. De nombreux modèles ont émergé de part et d'autre : XML, ODBMS, Map Reduce... Ces modèles ont pour objectif de résoudre les problèmes existants du modèle relationnel. Et pourtant, aucun n'a réussi à détrôner SQL, la variante la plus connue du modèle relationnel. Cela révèle tout d'abord un problème vis-à-vis du modèle relationnel tel qu'implémenté par SQL qui ne s'adapte pas à toutes les applications. Cela révèle aussi l'incapacité des nouveaux modèles à pallier les lacunes de SQL tout en conservant ses forces : son expressivité et sa capacité à assurer l'intégrité des données. Ces caractéristiques restent primordiales pour de nombreuses applications et ne peuvent donc pas être ignorées. Notre intuition est donc qu'il ne faut pas totalement mettre de côté le modèle relationnel de Codd [10], mais plutôt l'améliorer. Étant donné que seul le langage relationnel SQL a su s'imposer, l'évaluation des SGBD relationnels s'est toujours faite en ne considérant que celui-ci. De plus, les bancs d'essai existants considèrent le facteur de l'efficience comme le plus important à évaluer, probablement car c'est le critère qui dépend davantage de l'implémentation du langage faite par les SGBD que des variantes dialectiques du langage. Nous nous sommes donc donnée [i.e. donnés] pour objectif de définir un banc d'essai plus large permettant d'évaluer des modèles relationnels différents en prenant en compte des critères plus variés et tout aussi importants tels que la validité, la disponibilité, la sécurité et l'expressivité. Le banc d'essai ainsi défini a été implémenté pour deux SGBDR basés sur SQL : Oracle et PostgreSQL. L'implémentation pour des SGBDR basés sur des modèles différents étant laissée pour des travaux futurs. Les résultats obtenus nous ont tout d'abord permis de démontrer la pertinence de notre banc d'essai. Malgré le fait que les deux SGBD soient basés sur le langage SQL, le banc d'essai a révélé des différences pour la majorité des critères définis. Ainsi, Oracle se démarque en ce qui concerne la validité des données. Contrairement à PostgreSQL, il ne présente pas de lacunes pouvant compromettre l'intégrité des données. Oracle se démarque aussi en ce qui concerne la sécurité. Les mécanismes présents y sont plus complets et plus flexibles. PostgreSQL, lui, se démarque par rapport à l'expressivité du dialecte SQL utilisé. Des fonctionnalités primordiales sont présentes tandis qu'elles sont absentes sous Oracle. Au niveau de l'efficience, nos résultats révèlent une différence quant à la gestion des optimisations, car selon les fonctionnalités testées, le SGBD le plus efficient est différent. Cependant, aucun des SGBD ne se démarque. Pour finir, en ce qui concerne le critère de disponibilité des données, les résultats sont identiques pour les deux SGBD. Cette identification des lacunes propres à ces deux SGBD nous permettra par la suite de tirer des enseignements de ces problèmes de manière à ne pas les reproduire pour notre nouveau modèle.

Depuis l'antiquité jusqu'à aujourd'hui, le domaine de la logique a gagné une importance remarquable et contribue désormais à de nombreuses autres branches, telles que la philosophie, les mathématiques, la fabrication de matériel informatique, la linguistique, l'informatique, l'intelligence artificielle, etc. À chacun de ces scénarios correspondent des besoins spécifiques, qui vont d'exigences très concrètes, telles qu'une méthode d'inférence efficace, à des propriétés théoriques plus abstraites, telles qu'un système d'axiomes élégant. Étant donnée cette grande diversité d'utilisations, une palette hétéroclite de langages formels a été développée. Pendant de nombreuses années, les langages classiques (notamment la logique du premier ordre) étaient la seule alternative concevable, mais cet assortiment d'applications a rendu d'autres types de logiques également désirables dans de nombreuses situations. Imaginez que l'heure de choisir une logique pour une tâche spécifique arrive. Comment choisir la plus appropriée? Quelles propriétés devrions-nous rechercher? Comment "mesurer'' une logique par rapport aux autres? Ce sont des questions difficiles, et il n'existe pas de recette générale à suivre. Dans cette thèse, nous allons simplement restreindre ces questions à une famille particulière de logiques, et dans ce contexte, nous explorerons les aspects théoriques qui aideront à répondre à ces préoccupations. Beaucoup peut être découvert par une analyse attentive des cas les plus intéressants, et notre contribution sera développée selon cette philosophie. Les logiques modales propositionnelles offrent une alternative aux langages traditionnels. Elles peuvent être considérées comme un ensemble d'outils permettant de concevoir des logiques adaptées à des tâches précises, possédant un contrôle fin sur leur expressivité. De plus, il s'est avéré que les logiques modales possèdent un bon comportement computationnel, qui se trouve être robuste y compris malgré l'ajout d'extensions. Ces caractéristiques, parmi d'autres, ont élevé les logiques modales au rang d'alternatives désirables aux langages classiques. Dans ce thèse, nous allons présenter une nouvelle famille de logiques modales appelée logiques mémorielles. Les logiques modales traditionnelles permettent de décrire les structures relationnelles d'un point de vue local. Mais pourquoi ne pas changer cette structure? Nous voulons étudier l'ajout d'une structure de stockage explicite aux logiques modales, une mémoire, qui permet de modéliser un comportement dynamique à travers des opérateurs mémoriels explicites. Ces opérateurs sauvent ou restaurent de l'information vers et à partir de la mémoire. Naturellement, selon le type de structure de sauvegarde désiré et les opérateurs mémoriels disponibles, la logique résultante possèdera différentes propriétés qui valent la peine d'être étudiées. Cette thèse est organisée de la façon suivante. Dans le Chapitre 1, nous commençons par rappeler brièvement comment la logique modale est née, en montrant les différents points de vue historiques la concernant. Puis, nous présentons formellement la logique modale de base et un ensemble d'opérateurs étendus qui aident à capturer le ``goût'' modal de langages plus riches. Nous finissons ce chapitre en donnant un premier aperçu des logiques mémorielles, et montrons comment elles peuvent aider à modéliser l'état quand nous choisissons d'utiliser un ensemble comme une structure de sauvegarde. Le Chapitre 2 est dédié à la présentation détaillée des logiques mémorielles. Nous montrons quelques exemples qui peuvent être décrits en ajoutant un ensemble à des structures relationnelles usuelles, ainsi que les opérateurs ensemblistes usuels permettant l'ajout d'élément et le test d'appartenance. Puis, nous montrons que d'autres opérateurs mémoriels peuvent être envisagés, et nous discutons de la possibilité d'ajouter des contraintes à l'interaction entre la mémoire et les opérateurs modaux. Ces contraintes peuvent être vues comme une manière d'avoir un contrôle fin sur l'expressivité de la logique. Comme nous avons fait des changements aux logiques modales classiques, nous nous intéressons à l'analyse de l'impact de ces changements sur les logiques résultantes. Ainsi, le reste de ce chapitre présente une boite à outils logique basique avec laquelle nous pouvons analyser cette nouvelle famille de logiques. Cette boite à outils peut être vue comme un plan qui organise le reste de cette thèse et qui permet d'analyser les logiques mémorielles en termes d'expressivité, de complexité, d'interpolation et de théorie de la preuve. Le reste des chapitres consiste à étudier en détail chacun de ces aspects. Dans les Chapitres 3 et 4, nous explorons l'expressivité de plusieurs logiques mémorielles et nous étudions la décidabilité de leur problème de satisfiabilité. Dans les cas décidables, nous déterminons leur complexité. Nous analysons l'impact des différents opérateurs mémoriels considérés, et leur interaction. Nous étudions également d'autres conteneurs mémoriels, tels que la pile. Puis, dans le Chapitre 4, nous analysons l'interpolation de Craig et la définabilité de Beth pour certains fragments des logiques mémorielles. Nous étudions également les logiques mémorielles du point de vue de la théorie de la preuve. Dans les Chapitres 6 et 7, nous passons aux axiomatisations à la Hilbert et aux systèmes de tableaux, et nous caractérisons plusieurs fragments de la famille des logiques mémorielles, en utilisant principalement des techniques empruntées aux logiques hybrides. Nous concluons dans le Chapitre 8 avec quelques remarques, des problèmes ouverts et des directions pour de futures recherches. / From ancient times to the present day, the field of logic has gained significant strength and now it actively contributes to many different areas, such as philos- ophy, mathematics, linguistic, computer science, artificial intelligence, hardware manufacture, etc. Each of these scenarios has specific needs, that range from very concrete requirements, like an efficient inference method, to more abstract theoretical properties, like a neat axiomatic system. Given this wide diversity of uses, a motley collection of formal languages has been developed. For many years, classical languages (mainly classical first order logic) were the alternative, but this assortment of applications made other types of logics also attractive in many situations. Imagine that the time for choosing a logic for some specific task arrives. How can we decide which is the one that fits best? Which properties should we look for? How can we “measure” a logic with respect to others? These are not easy questions, and there is not a general recipe one can follow. In this thesis we are just going to restrict these questions to a particular family of logics, and in that context we will investigate theoretical aspects that help to answer some of these concerns. Much can be discovered by carefully analyzing appealing cases, and our contribution will be developed having that philosophy in mind. Propositional modal logics offer an alternative to traditional languages. They can be regarded as a set of tools that allow to design logics specially tailored for specific tasks, having a fine-grained control on their expressivity. Additionally, modal logics turned out to have a good computational behavior, which proved to be quite robust under extensions. These characteristics, among others, placed modal logics as an attractive alternative to classical languages. In this dissertation we are going to present a new family of modal logics called memory logics. Traditional modal logics enables to describe relational structures from a local perspective. But what about changing the structure? We want to explore the addition of an explicit storage structure to modal logics, a mem- ory, that allows to model dynamic behavior through explicit memory operators. These operators store or retrieve information to and from the memory. Natu- rally, depending on which type of storage structure we want, and which memory operators are available, the resulting logic will enjoy different properties that are worth investigating. The thesis is organized as follows. In Chapter 1 we start by giving a brief recap of how modal logic was born, showing the different historical perspectives used to look at modal logic. Then we formally present the basic modal logic and a set of extended operators that helps grasp the modal “flavor” of some richer languages. We finish this chapter by giving a first glance of memory logics, and showing how they can help to model state when we choose to use a set as storage structure. Chapter 2 is devoted to present memory logics in detail. We show some examples that can be described by adding a set to standard relational structures, and the usual set operators to add elements and test membership. We then show some other memory operators that can be considered, and we discuss the possibility of adding constraints to the interplay between memory and modal operators. These constraints can be regarded as a way to have a finer-grained control on the logic expressivity. Since we have made changes to classical modal logics, we are interested in analyzing the impact those changes cause in the resulting logics. Therefore, the rest of this chapter presents a basic logic toolkit through which we can analyze this new family of logics. This toolkit can be seen as an outline that organizes the rest of the thesis and that allows to analyze memory logics in terms of expressivity, complexity, interpolation and proof theory. The rest of the chapters investigate each of these aspects in detail. In Chap- ters 3 and 4 we explore the expressive power of several memory logics and we study the decidability of their satisfiability problem. In the decidable cases, we determine their computational complexity. We analyze the impact of the differ- ent memory operators we consider, and how they interact. We also study other memory containers, such as a stack. Then, in Chapter 5, we analyze Craig inter- polation and Beth definability for some memory logic fragments. We also study memory logics from a proof theoretical perspective. In Chapter 6 and 7 we turn to Hilbert style axiomatizations and tableau systems, and we characterize several fragments of the memory logic family mostly using techniques borrowed from hy- brid logics. We close in Chapter 8 with some concluding remarks, open problems and directions for further research.

L’ordinateur personnel, de bureau ou portable, permet le travail intellectuel et les activités créatives à travers une interaction directe et expressive. Mais l’impression de “directitude” disparaît quand les actions deviennent complexes, et l’expressivité est souvent favorisée au détriment d’une séparation spatiotemporelle, d’une charge cognitive, ou de suites complexes d’opérations. Cette thèse propose de mieux exploiter les périphériques d’entrée standard de façon à augmenter de façon directe la granularité, l’étendue, et la dimensionnalité des actions utilisateur. Nous montrons d’abord que la granularité des mouvements du pointeur peut être augmentée sans déranger son fonctionnement habituel si la fonction de transfert du pointage prend en compte les périphériques, les capacités de l’utilisateur, et le modèle de données manipulé. Une limite de l’interaction subpixel ainsi permise est la résolution utile (le plus petit déplacement pouvant être produit avec un périphérique), pour laquelle nous proposons un protocole expérimental.Nous étudions ensuite l’edge-scrolling, une technique qui étend le déplacement d’objets et la sélection au-delà des limites d’une vue en la faisant défiler. Nous montrons plusieurs problèmes d’utilisabilité par l’examen de 33 implémentations, un sondage et des expériences contrôlées. Nous évitons ces problèmes en proposant push-edge et slide-edge, qui montrent des performances similaires aux techniques existantes. Enfin, nous décrivons trois utilisations réussies de l’ordinateur portable comme instrument de musique permettant le contrôle simultané temps-réel de plusieurs paramètres sonores, en détaillant quelques problèmes de conception. / Desktop and laptop personal computers enable knowledge work and creative activities by supporting direct and expressive interaction. But the feeling of directness often disappears when users perform complex actions: expressiveness is ensured at the cost of spatiotemporal separation, cognitive load, or complex operation sequences. This thesis proposes to solve this problem by harnessing the unexploited capabilities of standard input devices and familiar actions performed on them. We investigate how this enables direct increases of the granularity, extent, and dimensionality of user actions. First, we show that the granularity of pointer movements can be increased a hundredfold without impeding normal behavior if pointing transfer functions include device characteristics, user capabilities, and the manipulated data model, thus allowing subpixel interaction. This is limited by the useful resolution, the smallest displacement a user can produce using a pointing device, for which we propose an experimental protocol.Second, we study the design space of a widely used technique, edge-scrolling, that extends dragging actions past a viewport edge by scrolling. We reverse engineer 33 existing implementations, and highlight usability problems through a survey and experiments. We also propose push-edge and slide-edge scrolling, two position control techniques that provide performance comparable to rate control without the shortcomings. Third, we describe three ways of using a standard laptop as a musical instrument, allowing simultaneous multiparametric control of sound synthesis in real time, together with design considerations and examples of successful uses.

La focalisation prosodique désigne le soulignement d’un constituant dans un énoncé au moyen de différentes ressources prosodiques, en particulier l’accentuation et l’intonation. Plusieurs fonctions sont attribuées à la focalisation : le marquage des différentes catégories de focus, ainsi que des fonctions emphatiques (ici appelées insistance et expressivité). Cette thèse a pour principal but de savoir si la focalisation et ses fonctions présentent des propriétés spécifiques dans le phonogenre de la parole interprétée, c’est-à-dire l’oralisation d’un texte écrit mémorisé au préalable par le locuteur (généralement un comédien). Cette question présente un intérêt pour la linguistique et la phonétique à plusieurs titres. Tout d’abord, les différences de réalisation prosodique entre les fonctions de la focalisation sont encore mal connues. Par ailleurs, peu d’études ont été consacrées aux caractéristiques prosodiques de la parole interprétée. Enfin, notre thèse présente un apport sur le plan méthodologique à travers le protocole relativement novateur de ses deux expériences. Dans une expérience de production, des locuteurs ont reproduit des conversations spontanées en parole lue et en parole interprétée. Un groupe d’experts en prosodie a ensuite relevé les occurrences de focalisation dans le corpus et a effectué une classification fonctionnelle de ces occurrences. Nous avons également mené une expérience de perception afin de comparer la réalisation des fonctions de la focalisation indépendamment du phonogenre. Malgré un taux d’accord entre experts relativement faible (ce qui soulève plusieurs questions méthodologiques et théoriques), nos analyses révèlent plusieurs résultats originaux. La fréquence d’occurrence de la focalisation est la plus élevée en parole interprétée, suivie de la parole lue. Ce résultat confirme notre prédiction et suggère que la parole interprétée est un phonogenre favorable à l’étude de la focalisation. Une forte relation est observée entre la fonction d’insistance et le trait d’accentuation initiale, ce qui confirme de nombreuses études précédentes. Le phonogenre se révèle en revanche avoir très peu d’influence sur la réalisation de la focalisation et de ses fonctions. Ce résultat est dû selon nous à un manque de données et au fait que certains traits prosodiques n’ont pas été pris en compte dans l’analyse. / Prosodic highlighting refers to the distinction of a constituent through various prosodic means, especially accentuation and intonation. It is taken to fulfill several functions: marking the different types of focus, as well as emphatic functions (named here “insisting” and “expressiveness”). The main goal of this thesis is to determine whether prosodic highlighting and its functions display specific features in interpreted speech, a speaking style that can be defined as the oralization of a written text previously memorized by the speaker (typically an actor). This question is relevant for linguistics and phonetics on several counts. First, little is still known about prosodic differences between functions of prosodic highlighting. Moreover, few studies have analyzed the prosodic characteristics of interpreted speech. Finally, through their innovative protocols, the two experiments described in this thesis present a methodological contribution. A production experiment consisted in having speakers replicate spontaneous conversations in read and interpreted speech. A group of experts then annotated the occurrences of prosodic highlighting in the corpus, and assigned a function to each occurrence. A perception experiment was also led in order to compare the realization of each function independently of speaking style. Despite a relatively low agreement rate between experts (which raises several methodological and theoretical questions), our analyses reveal several important results. The frequency of occurrence of prosodic highlighting is highest in interpreted speech, followed by read speech. This confirms our prediction and suggests that interpreted speech is more suited to the study of prosodic highlighting than other speaking styles. A strong association is observed between insisting and initial secondary accent, which confirms many previous studies. However, there is almost no influence of speaking style on the realization of prosodic highlighting and its functions. We attribute this result to a lack of data and to the fact that some prosodic features were not taken into account in the analysis.

Les environnements virtuels permettent de représenter des personnes par des humains virtuels ou avatars. Le sentiment de présence virtuelle entre utilisateurs est renforcé lorsque l’avatar ressemble à la personne qu’il représente. L’avatar est alors classiquement un clone de l’utilisateur qui reproduit son apparence et sa voix. Toutefois, la possibilité de cloner l’expressivité des gestes d’une personne a reçu peu d’attention jusqu’ici. Expressivité gestuelle combine le style et l’humeur d’une personne. Des paramètres décrivant l’expressivité ont été proposés dans des travaux antérieurs pour animer les agents conversationnels. Dans ce travail, nous nous intéressons à l’expressivité des mouvements du poignet. Tout d’abord, nous proposons des algorithmes pour estimer trois paramètres d’expressivité à partir des trajectoires dans l’espace du poignet : la répétition, l’étendue spatiale et l’étendue temporelle. Puis, nous avons mené une étude perceptive sur la pertinence de l’expressivité des gestes pour reconnaître des personnes. Nous avons animé un agent virtuel en utilisant l’expressivité estimée de personnes réelles, et évalué si des utilisateurs peuvent reconnaître ces personnes à partir des animations. Nous avons constaté que des gestes répétitifs dans l’animation constituent une caractéristique discriminante pour reconnaître les personnes, tandis que l’absence de répétition est associée à des personnes qui répètent des gestes ou non. Plus important, nous avons trouvé que 75% ou plus des utilisateurs peuvent reconnaître une personne (parmi deux proposée) à partir d’animations virtuelles qui ne diffèrent que par leurs étendues spatiales et temporelles. L’expressivité gestuelle apparaît donc comme un nouvel indice pertinent pour le clonage d’une personne / Virtual environments allow human beings to be represented by virtual humans or avatars. Users can share a sense of virtual presence is the avatar looks like the real human it represents. This classically involves turning the avatar into a clone with the real human’s appearance and voice. However, the possibility of cloning the gesture expressivity of a real person has received little attention so far. Gesture expressivity combines the style and mood of a person. Expressivity parameters have been defined in earlier works for animating embodied conversational agents.In this work, we focus on expressivity in wrist motion. First, we propose algorithms to estimate three expressivity parameters from captured wrist 3D trajectories: repetition, spatial extent and temporal extent. Then, we conducted perceptual study through a user survey the relevance of expressivity for recognizing individual human. We have animated a virtual agent using the expressivity estimated from individual humans, and users have been asked whether they can recognize the individual human behind each animation. We found that, in case gestures are repeated in the animation, this is perceived by users as a discriminative feature to recognize humans, while the absence of repetition would be matched with any human, regardless whether they repeat gesture or not. More importantly, we found that 75 % or more of users could recognize the real human (out of two proposed) from an animated virtual avatar based only on the spatial and temporal extents. Consequently, gesture expressivity is a relevant clue for cloning. It can be used as another element in the development of a virtual clone that represents a person

Cette thèse s'inscrit dans le cadre de la synthèse de parole à partir du texte. Elle traite plus précisément du procédé de création de voix en synthèse par sélection d'unités. L'état de l'art repose pour cela sur l'enregistrement d'un locuteur pendant une à deux semaines, suivant un script de lecture de plusieurs dizaines de milliers de mots. Les 5 à 10 heures de parole collectées sont généralement révisées par des opérateurs humains, pour en vérifier la segmentation phonétique et ainsi améliorer la qualité finale de la voix de synthèse.La lourdeur générale de ce procédé freine considérablement la diversification des voix de synthèse ; aussi en proposons-nous ici une rationalisation. Nous introduisons une nouvelle unité, appelée "sandwich vocalique", pour l'optimisation de la couverture des scripts de lecture. Sur le plan phonétique, cette unité offre une meilleure prise en compte des limites segmentales de la synthèse par sélection que les unités traditionnelles (diphones, triphones, syllabes, mots, etc.). Sur le plan linguistique, un nouvel enrichissement contextuel nous permet de mieux focaliser la couverture, sans négliger les aspects prosodiques. Nous proposons des moyens d'accroître le contrôle sur les phrases du script lecture, tant dans leur longueur que dans leur pertinence phonétique et prosodique, afin de mieux anticiper le contenu du corpus de parole final et de rendre automatisable la tâche de segmentation. Nous introduisons également une alternative à la stratégie classique de condensation de corpus en mettant au point un algorithme semi-automatique de création de phrases, grâce auquel nous accroissons de 30 à 40% la densité linguistique du script de lecture.Ces nouveaux outils nous permettent d'établir un procédé très efficace de création de voix de synthèse, procédé que nous validons à travers la création et l'évaluation subjective de nombreuses voix. Des scores perceptifs comparables à l'approche traditionnelle sont ainsi atteints dès 40 minutes de parole (une demi-journée d'enregistrement) et sans post-traitement manuel. Enfin, nous mettons à profit ce résultat pour enrichir nos voix de synthèse de diverses composantes expressives, multi-expressives et paralinguistiques.

La synthèse de parole expressive constitue aujourd'hui un nouveau défi . Un moyen direct de rendre la synthèse expressive consiste à la contrôler en temps réel par les gestes d'un opérateur. Notre recherche s'est donc déroulée selon deux axes : d'une part la modi fication prosodique (hauteur et durée) de la parole enregistrée, et d'autre part la synthèse de voyelles à partir d'un modèle de source glottique. Concernant la modifi cation prosodique, nous avons implémenté un algorithme temps réel permettant la modifi cation conjointe de la hauteur et de la durée d'une phrase enregistrée. Grâce à cet outil, nous avons mené des expériences visant à valider la possibilité de modi fier la prosodie grâce au geste. Nos expériences ont montré la possibilité de reproduire avec précision une intonation donnée grâce au geste manuel. Le second axe de notre recherche s'est focalisé sur la réalisation d'un synthétiseur de voyelles, dont on peut modi fier la qualité vocale. La première étape a consisté à implémenter une version temps réel de la synthèse de l'onde de débit glottique, ainsi que des apériodicités de la source vocale. Nous pouvons ainsi contrôler la fréquence fondamentale, l'eff ort vocal, la tension, le souffle, les apériodicités structurelles et les di fférents mécanismes laryngés. Une attention particulière a été apportée à la réalisation du phonétogramme, ainsi qu'aux correspondances perceptives entre les paramètres du modèle et les dimensions vocales. Notre étude permet d'envisager à terme la modifi cation conjointe, interactive, des composantes prosodiques et de qualité vocale.

The doctoral dissertation introduces independence-friendly (IF) modal logic as an extension of standard modal logic. Making use of the notion of uniform strategy, a game-theoretical interpretation of IF modal logic is formulated. It is shown that under this interpretation, IF modal logic has greater expressive power than standard modal logic, and can be translated into first-order logic. However, when restricted to a simple tense-logical setting (evaluation over strict linear orders), its expressive power coincides with standard tense logic. The syntax of IF modal logic can be modified to allow independence of modal operators from conjunctions and disjunctions. It is shown that the resulting modal logic can no longer be translated into first-order logic. Two further interpretations of the language of IF modal logic are given, one in terms of backwards-looking operators, the other algebraic. The dissertation contains an extensive discussion of tenses in linguis- tics, and explains how the 'backwards-looking operators' interpretation of IF tense logic makes it possible to formally distinguish between two types of independence appearing in connection with tense evaluation. It is argued that the linguistic critique against scope theories of tense becomes less appealing when this distinction is made.

Dans le cadre de la vérification formelle de programmes, nous étudions des systèmes placés dans un environnement extérieur : il s'agit de guider ou contrôler le système pour qu'il satisfasse certaines propriétés. Pour modéliser l'écoulement du temps, nous nous intéressons aux systèmes hybrides et aux logiques temporisées. Nous étudions les systèmes hybrides o minimaux pondérés et établissons que ce modèle est expressif mais analysable puisque le model checking ainsi que le contrôle optimal sont décidables, ces problèmes étant indécidables pour les automates temporisés. Nous étudions également les logiques temporisées et montrons que la logique TPTL est strictement plus expressive que MTL, prouvant une conjecture énoncée par Alur et Henzinger au début des années 1990. Enfin nous introduisons une classe d'automates paramétrés par des opérateurs et obtenons des résultats génériques d'expressivité entre automates et logiques, qui peuvent notamment s'appliquer à MTL+Past.

Le concept de réversibilité est ancien, mais il soulève de nos jours beaucoup d'intérêt. Il est en effet exploité dans de nombreux domaines tels que la conception de circuits, le débogage et le test de programmes, la simulation et l'informatique quantique. L'idée d'un modèle de programmation réversible peut se montrer particulièrement intéressante pour la construction de systèmes sûrs de fonctionnement, ne serait-ce que parce que plusieurs techniques connues pour la construction de tels systèmes exploitent une forme ou une autre de retour en arrière ou de reprise. Nous poursuivons dans cette thèse l'étude entreprise avec CCS réversible par Vincent Danos et Jean Krivine, en définissant un pi-calcul d'ordre supérieur réversible (rhopi). Nous prouvons que le modèle obtenu est causalement cohérent, et que l'on peut encoder fidèlement rhopi dans une variante du pi-calcul d'ordre supérieur. Nous définissons également une primitive de reprise à grain fin qui permet de contrôler le retour en arrière dans une exécution concurrente. Nous spécifions formellement la sémantique de cette primitive, et nous montrons qu'elle possède de bonnes propriétés, y compris en présence d'opérations de reprise concurrentes. Enfin nous définissons un algorithme concurrent implantant cette primitive de reprise et ous montrons que cet algorithme respecte la sémantique définie.