La plupart des scénarios multimédia interactifs sont basés sur des spécifications informelles, il n'est donc pas possible de vérifier formellement des propriétés de ces systèmes. Nous préconisons la nécessité d'un modèle général et formel. Partitions interactives est un formalisme pour décrire des scénarios multimédia interactifs. Nous proposons une nouvelle sémantique pour les partitions interactives basée sur les structures d'événements temporisés. Avec une telle sémantique, nous pouvons spécifier des propriétés pour le système, en particulier, des propriétés sur les traces, qui sont difficiles à préciser avec la programmation par contraintes. Nous présentons également une sémantique opérationnelle des partitions interactives basée sur le calcul non-déterministe, temporisé, concurrent, par contraintes (ntcc) et nous rapportons la sémantique operationelle à la semantique en structures d'événements temporisés. Avec la sémantique opérationnelle, nous pouvons décrire formellement le comportement d'un scenario dont les durées des objets temporels peuvent être des intervalles d'entiers arbitraires. La sémantique opérationnelle est obtenue à partir de la sémantique en structures d'événements temporisés de la partition interactive. Pour fournir une telle traduction, nous avons d'abord défini la forme normale d'une structure d'événements temporisés, dans laquel les événements liés avec une durée zéro sont regroupés en un seul. Nous avons également défini la notion de structures d'événements temporisés répartissables, de telle sorte que son graphe de contraintes peut être expédié en se fondant uniquementsur la propagation locale. Nous croyons que la sémantique opérationnelle basée sur ntcc offre certains avantages par rapport à la sémantique des partitions interactives basée sur des réseaux de Petri; par exemple, les durées des objets temporels peuvent être des intervalles d'entiers arbitraires, tandis que dans la plupart des modèles de partitions interactives, les intervalles ne peut être utilisés que pour représenterles relations telles que l'égalité et les inégalités. Nos modèles ntcc de partitions interactives sont exécutés en utilisant Ntccrt, un interprète temps réel pour ntcc. Nos modèles peuvent également être vérifiés automatiquement en utilisant ntccMC, un vérificateur pour ntcc, de temps borné, basée sur les automates finis, que nous introduisons dans cette thèse. En utilisant ntccMC, nous pouvons vérifier des propriétés de logique de temps linéaire avec des contrantes (CLTL). Dans cette thèse, nous introduisons deux extensions du formalisme de partitions interactives:(1) l'une pour gérer le traitement audio en utilisant le langage de programmation français Faustet (2) l'autre pour traiter des condition et des branchements, permettant de spécifier des choix et des boucles. Pour la première extension, nous présentons une sémantique basée sur les structures d'événements temporisés et des idées sur la façon de définir une sémantique opérationnelle. Pour la deuxième extension, nous présentons une mise en oeuvre et la comparaison des résultats du jitter relative moyenne d'une implémentation d'un arpège base sur l'algorithme de Karplus-Strong par rapport aux implémentations existants écrits dans Pure Data. Nous définissons aussi un format de sauvegarde XML pour les partitions interactives et pour la extension avec branchement conditionnel. Un format de sauvegarde est crucial pour assurer la persistance des partitions. / Technology has shaped the way on which we compose and produce music. Notably, the invention of microphones and computers pushed the development of new music styles in the 20th century. In fact, several artistic domains have been benefiting from such technology developments ; for instance, Experimental music, non-linear multimedia, Electroacoustic music, and interactive multimedia. In this dissertation, we focus on interactive multimedia.Interactive multimedia deals with the design of scenarios where multimedia content and interactive events are handled by computer programs. Examples of such scenarios are multimedia art installations, interactive museum exhibitions, some Electroacoustic music pieces, and some Experimental music pieces. Unfortunately, most interactive multimedia scenarios are based on informal specifications, thus it is not possible to formally verify properties of such systems. We advocate the need of a general and formal model. Interactive scores is a formalism to describe interactive multimedia scenarios. We propose new semantics for interactive scores based on timed eventstructures. With such a semantics, we can specify properties for the system, in particular, properties about traces, which are difficult to specify as constraints. In fact, constraints are an important part of the semantic model of interactive scores because the formalism is based on temporal constraints among the objects of the scenario. We also present an operational semantics of interactive scores based on the non-deterministic timed concurrent constraint (ntcc) calculus and we relate such a semantics to the timed event structures semantics. With the operational semantics, we formally describe the behavior of a score whose temporal object durations can be arbitrary integer intervals. The operational semantics is obtained from the timed event structures semantics of the score. To provide such a translation, we first define the normal form of a timed event structure in which events related with zero-duration delays are collapsed into a single one. We also define the notion of dispatchable timed event structures. Event structures such that its constraint graph can be dispatched by relying only on local propagation.We believe that operational semantics in ntcc offers some advantages over existing Petri nets semantics for interactive scores; for instance, the duration of the temporal objects can be arbitrary integer intervals, whereas inprevious models of interactive scores, such durations can only be intervals to represent equalities and inequalities. In this dissertation, we also introduce two extensions of the formalism of interactive scores : (1) one to handle audio processing using the Fast AUdio Stream (Faust) languageand (2) another one to handle conditional branching, allowing designers to specify choices and loops. For the first extension, we present a timed event structures semantics and ideas on how to define operational semantics. For the second extension, we present an implementation and results comparing the average relative jitter of an implementation ofan arpeggio based on Karplus-Strong with respect to existing implementations of Karplus written in Pure Data. We also define a XML file format for interactive scores and for the conditional branching extension. A file format is crucial to assure the persistence of the scores. Ntcc models of interactive scores are executed using Ntccrt, a real-time capable interpreter for ntcc. They can also be verified automatically using ntccMC, a bounded-time automata based model checker for ntcc which we introduce in this dissertation. Using ntccMC, we can verify properties expressed on constraint linear-time logic. Ntcc has been used in the past, not only for multimedia interaction models, but alsofor system biology, security protocols and robots.

La sémantique des jeux permet l'étude et la modélisation abstraite des langages de programmation d'un point de vue mathématique, en gardant assez d'informations concrètes sur la structure des programmes, mais en laissant de côté les détails superflus. Durant mon doctorat, j'ai travaillé sur l'association de la sémantique des jeux avec les structures d'événements pour proposer des modèles dénotationnels vraiment concurrents de langages concurrents d'ordresupérieur. Dans un premier temps, je construis un modèle réalisant cette association, qui retient suffisamment d'informations sur le comportement des programmes pour interpréter adéquatement une grande variété de langages concurrents et non déterministes pour des notions fines de convergences. La construction de ce modèle se base surl'introduction de symétrie afin d'établir que le modèle forme une catégorie cartésienne fermée. Dans un second temps, je propose une généralisation dans ce cadre des notions d'innocence et de bon parenthésage, essentielles en sémantiquedes jeux pour comprendre les effets calculatoires, et résolvant ainsi des problèmes ouverts de la sémantique des jeux concernant l'innocence concurrente et non-déterministe. Dans un dernier temps je propose une interprétation dans ce modèle, de langages concurrents avec mémoire faible, un des premiers travaux de sémantique dénotationnelle pour ce type de langages. Bien que théoriques, ces modèles sont compositionnels et basés sur des ordres partiels, et donc pourraient permettre de faire passer la vérification de programmes concurrents à l'échelle (une problématique importante du domaine). / Game semantics is an effective tool to study and model abstractly programming languages from a mathematical point of view, by keeping enough concrete information on the structure of programs but yet leaving aside superfluous details. During my PhD thesis, I worked on merging game semantics with event structures to propose truly concurrent denotational models of higher-order concurrent languages. In the first part, I build a model based on this merge, retaining enough information about the behaviour of programs to interpret adequately a large variety of concurrent programming languages for various notions of convergence. The construction of this model is based on the introduction of symmetry to prove that the model is indeed in a cartesian-closed category. In the second part, I propose a generalization, in this setting, of innocence and well-bracketing, key notions in game semantics to understand the computational effects, and thusly closing openproblems of game semantics about concurrent and nondeterministic innocence.In the last part, I propose an interpretation in this model of concurrent languages with weak shared memory, one of the first works of denotational semantics for these kinds of languages. Althoughtheoretical, these models are compositional and based on partial orders, and thus could permit scaling verification of concurrent programs (an important problem of the domain).

La sémantique des jeux est une sémantique dénotationnelle centrée sur l’interaction : preuves et programmes y sont représentés par des stratégies modélisant, par le flot d’exécution, leur manière de réagir à leur environnement. Malgré cette présentation intensionnelle, les sémantiques de jeux ne suffisent pas à capturer certaines informations calculatoires annexes au flot d’exécution telles que, par exemple, la production de témoins en logique du premier ordre ou la consommation de ressources dans les langages de programmation. Dans cette thèse nous proposons un enrichissement du modèle des jeux concurrent à base de structures d’événements permettant de garder trace de ces informations.Nous construisons d’abord un modèle de jeux concurrent dans lequel les coups joueurs d’une stratégie sont annotés par les termes d’une théorie (in)équationnelle. Cette théorie est un paramètre de notre modèle et les annotations permettent de refléter de manière compacte des informations d’exécution n’ayant pas d’influence sur le flot d’exécution. Nous montrons que le modèle ainsi construit préserve la structure catégorique compacte fermée du modèle sans annotation.Nous explorons ensuite l’expressivité de notre modèle et présentons deux interprétations nouvelles en sémantique des preuves et des programmes : l’une interprétant les preuves de la logique classique du premier ordre par des stratégies concurrentes avec échange de témoins, donnant une version compositionnelle au théorème de Herbrand ; l’autre permettant de refléter les aspects quantitatifs liés à la consommation de ressources telles que le temps, dans l’exécution de programmes concurrents d’ordre supérieur avec mémoire partagée. / This thesis presents a general framework for enriching causal concurrent games model with annotations. These annotations can be viewed as meta-data on strategies: they are modified throughout interactions but do not affect their general flow of control. These data can be of various nature, in particular our enrichment is parametrised over any multi-sorted equational theory and can also reflect structure upon these data such as a partial order. From a semantics point of view, this construction is motivated by problems from both logic and programming languages: On the logic side, the annotated games model specialised to first-order terms enables us to give a novel interpretation of first-order classical proofs as concurrent strategies carrying first-order witnesses. In particular this answer the question of giving a compositional version to Herbrand’s theorem while avoiding the usual proof sequentialization of other denotational approaches. On the programming language side, annotations on games offer intrinsic quantitative models. We show that those can be used to provide denotational semantics for resource consumption analysis of concurrent higher order programming language with shared memory.These enrichments, strongly connected to the causal structure of concurrent games, give an argument in favor of a causal meaning of computations.