Raffinement temporel et exécution parallèle dans un langage synchrone fonctionnel

In this thesis, we are interested in the ReactiveML language, which extends ML with constructs inspired from synchronous languages. The idea of these languages is to divide the execution of a program into a succession of discrete logical instants. It results in a deterministic model of concurrency that can be compiled to sequential imperative code. The main application domain of ReactiveML is discrete simulation, for instance of sensor networks. We focus here on the problem of large scale simulation that raises two questions: can we program such simulations easily and modularly? can we execute them efficiently?We answer the first question by proposing an extension of the synchronous model called reactive domains. It allows the creation of local instants, invisible from the outside. It enables temporal refinement, that is, to replace an approximate model of a system with a more detailed version without changing its external behavior. We describe the formal semantics of this construct as well as static analyses, presented as type-and-effect systems, to ensure the soundness of programs in the extended setting. Our second contribution is several parallel implementations of the language to allow the scaling of simulations. We first describe an implementation based on threads communicating by shared memory and using work stealing, and then a second one based on processes communicating by message passing.Nous nous intéressons dans ce manuscrit au langage ReactiveML, qui est une extension de ML avec des constructions inspirées des langages synchrones. L'idée de ces langages est de diviser l'exécution d'un programme en une suite d'instants logiques discrets. Cela permet de proposer un modèle de concurrence déterministe que l'on peut compiler vers du code séquentiel impératif. La principale application de ReactiveML est la simulation discrète, par exemple de réseaux de capteurs. Nous cherchons ici à programmer des simulations à grande Échelle, ce qui pose deux questions: sait-on les programmer de façon simple et modulaire? sait-on ensuite exécuter ces programmes efficacement?Nous répondons à la première question en proposant une extension du modèle synchrone appelée domaines réactifs. Elle permet de créer des instants locaux invisibles de l'extérieur. Cela rend possible le raffinement temporel, c'est-à-dire le remplacement d'une approximation d'un système par une version plus détaillée sans changer son comportement externe. Nous développons dans ce manuscrit la sémantique formelle de cette construction ainsi que plusieurs analyses statiques, sous forme de systèmes de types-et-effets, garantissant la sureté des programmes dans le langage étendu.Enfin, nous montrons également plusieurs implémentations parallèles du langage pour tenter de répondre à la question du passage à l'échelle des simulations. Nous décrivons tout d'abord une implémentation avec threads communiquant par mémoire partagée et basée sur le vol de tâches, puis une seconde implémentation utilisant des processus lourds communiquant par envoi de messages.PARIS-BIUSJ-Mathématiques rech (751052111) / SudocSudocFranceF