Tout comme l'indique Whorf, nous analysons le monde à l'intérieur du cadre sémantique de notre langue maternelle. Il en va de même pour la résolution de problèmes à l'aide de langages de programmation. Les possibilités offertes par un langage et sa syntaxe façonnent notre conception du domaine du problème. Ainsi, si la langue forme notre pensée, les mots qui la composent ne sont parfois pas suffisants pour exprimer toute la richesse de nos idées. Par exemple, les spécialistes de domaines particuliers utilisent souvent un jargon. Pour s'en convaincre, il suffit d'écouter la conversation de deux professionnels d'un domaine qui nous est inconnu. Nous constatons qu'ils ne parlent pas tout à fait la même langue que nous. Ils s'échangent des idées et discutent de concepts en utilisant des mots et des expressions qui semblent étranges. Ainsi, les experts d'un même domaine développent leur propre jargon i.e. un langage spécifique à leur domaine d'affaire. Cette nouvelle langue leur permet de communiquer leur pensée de façon rapide et précise sans s'encombrer des détails et des lacunes de la langue « hôte ». Dans le présent travail, nous posons un regard sur les constructions linguistiques permettant la remise en valeur de la construction de langages spécifiques à un domaine d'affaire (DSL) : système de types dynamiques, métaprogrammation et éléments syntaxiques divers. Nous réalisons un survol des DSLs. Que sont-ils? Quand, comment et pourquoi les construisons-nous? Nous voyons aussi quelques patrons de conception de DSLs. Finalement, nous appliquons la théorie exposée à un problème réel. Nous montrons les avantages apportés par l'élaboration et l'utilisation de DSLs dans le cadre du développement de logiciels. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Langages dynamiques, DSL, Métaprogrammation, Groovy.

La multiplication des environnements logiciels pour la Modélisation & Simulation DEVS pose un problème de collaboration à la communauté scientifique. En effet, l'utilisation d'outils disparates rend l'échange, la réutilisation et la comparaison de modèles très difficiles, empêchant les scientifiques de s'appuyer sur des travaux précédents pour construire leurs modèles. L'interopérabilité des outils n'est pas le seul problème soulevé par le besoin de modèles toujours plus complexes. Au fur et à mesure que les modèles grossissent, leur développement devient plus difficile, notamment en termes de détection des erreurs de conception. D'autre part, la simulation de ces modèles demande de plus en plus de ressources. Par conséquent, il est nécessaire de concevoir des techniques pour améliorer la performance des simulateurs et pour fournir des fonctionnalités de vérification de modèle afin d'assister les scientifiques dans la conception de leurs modèles. Dans cette thèse, nous proposons deux approches innovantes pour la M&S DEVS qui s'attaquent aux problèmes susmentionnés. La première contribution décrite dans ce document est un environnement basé sur les modèles pour modéliser des systèmes avec le formalisme DEVS, intitulé SimStudio. Cet environnement repose sur l'Ingénierie Dirigée par les Modèles pour fournir un cadriciel de haut niveau dans lequel les scientifiques peuvent créer, éditer et visualiser des modèles, et générer automatiquement un ensemble d’artefacts, notamment des spécifications de modèles compatibles avec différents simulateurs DEVS. Le noyau de SimStudio est un métamodèle de DEVS, indépendant de toute plateforme, qui fournit un format pivot pour la représentation des modèles DEVS. En se basant sur ce métamodèle, nous avons développé plusieurs fonctionnalités de vérification de modèle ainsi que plusieurs transformations de modèle pouvant être utilisées pour générer automatiquement de la documentation, des diagrammes ou du code ciblant diverses plateformes DEVS. Ainsi, SimStudio fournit une preuve de concept des capacités d’intégration qu’un standard DEVS pourrait fournir ; en fait, le métamodèle présenté dans cette thèse pourrait potentiellement servir de base de réflexion pour un tel standard. La seconde contribution de cette thèse est DEVS-MetaSimulateur (DEVS-MS), une bibliothèque DEVS qui utilise la métaprogrammation pour générer des exécutables de simulation spécialisés et optimisés pour le modèle qu’ils traitent. Pour ce faire, la bibliothèque effectue un grand nombre d’opérations durant la compilation, résultant en un code de simulation où une grande partie de l’overhead de simulation a été éliminé. Les tests que nous avons effectués ont montré que les programmes générés étaient très efficaces, mais le gain de performance n’est pas la seule caractéristique intéressante de DEVS-MS. En effet, grâce à la métaprogrammation, DEVS-MS peut également partiellement vérifier à la compilation que les modèles sont corrects, c’est-à-dire que leurs caractéristiques sont bien conformes au formalisme DEVS. Les erreurs de modélisation sont ainsi détectées et signalées très tôt dans le cycle de développement, et avec un taux de détection bien meilleur que ne le permettrait des tests classiques. / The multiplication of software environments supporting DEVS Modeling & Simulation is becoming a hindrance to scientific collaboration. Indeed, the use of disparate tools in the community makes the exchange, reuse and comparison of models very difficult, preventing practitioners from building on previous works to devise models of ever-increasing complexity. Tool interoperability is not the only issue raised by the need for models of higher and higher complexity. As models grow, their development becomes more error-prone, and their simulation becomes more resource-consuming. Consequently, it is necessary to devise techniques for improving simulators performance and for providing thorough model verification to assist the practitioner during model design. In this thesis, we propose two innovative approaches for DEVS Modeling & Simulation that tackle the aforementioned issues. The first contribution described in this document is a model-driven environment for modeling systems with the DEVS formalism, named SimStudio. This environment relies on Model-Driven Engineering to provide a high-level framework where practitioners can create, edit and visualize models, and automatically generate multiple artifacts, most notably model specifications compatible with various DEVS simulators. The core of SimStudio is a platform-independent metamodel of the DEVS formalism, which provides a pivot format for DEVS models. Based on this metamodel, we developed several model verification features as well as many model transformations that can be used to automatically generate documentation, diagrams or code targeting various DEVS platforms. Thus, SimStudio gives a proof of concept of the integration capabilities that a DEVS standard would provide; as a matter of fact, the metamodel presented in this thesis could possibly serve as a basis for such a standard. The second contribution of this thesis is DEVS-MetaSimulator (DEVS-MS), a DEVS library relying on metaprogramming to generate simulation executables that are specialized and optimized for the model they handle. To do so, the library performs many computations during compilation, resulting in a simulation code where most overhead have been eliminated. The tests we conducted showed that the generated programs were very efficient, but the performance gain is not the only feature of DEVS-MS. Indeed, through metaprogramming, DEVS-MS can also assert the correctness of models by verifying model characteristics at compile-time, detecting and reporting modeling errors very early in the development cycle and with better confidence than what could be achieved with classical testing.

Ce mémoire a pour thèse que les fonctions devraient être transparentes lors de la phase de métaprogrammation. En effet, la métaprogrammation se veut une possibilité pour le programmeur d’étendre le compilateur. Or, dans un style de programmation fonctionnelle, la logique du programme se retrouve dans les définitions des diverses fonctions le composant. Puisque les fonctions sont généralement opaques, l’impossibilité d’accéder à cette logique limite les applications possibles de la phase de métaprogrammation. Nous allons illustrer les avantages que procurent les fonctions transparentes pour la métaprogrammation. Nous donnerons notamment l’exemple du calcul symbolique et un exemple de nouvelles optimisations désormais possibles. Nous illustrerons également que la transparence des fonctions permet de faire le pont entre les datatypes du programme et les fonctions. Nous allons également étudier ce qu'implique la présence de fonctions transparentes au sein d'un langage. Nous nous concentrerons sur les aspects reliés à l'implantation de ces dernières, aux performances et à la facilité d'utilisation. Nous illustrerons nos propos avec le langage Abitbol, un langage créé sur mesure pour la métaprogrammation. / Our main thesis is that functions should be transparent during the metaprogramming stage. Metaprogramming is intended as a possibility for the programmer to extend the compiler. But in a functional programming style, the program logic is found in the definition of its functions. Since functions are generally opaque, it is impossible for the programmer to access this information and this limits the metaprogramming possibilities. We will illustrate the benefits of transparent functions for metaprogramming. We will give the example of symbolic computation and also show new forms of optimizations now available at the metaprogramming stage. We will also illustrate that transparency allows us to bridge the gap between the datatypes of a program and its functions. We will also examine how transparent functions affects other aspects of the language. We will focus on how to implement them, their performance impact and their ease of use. We illustrate our thesis with Abitbol, a language designed for metaprogramming.

Cette thèse s'intéresse à la métathéorie de la théorie des types intuitionniste. Les systèmes que nous considérons sont des variantes de la théorie des types de Martin-Löf ou du Calcul des Constructions, et nous nous intéressons à la cohérence de ces systèmes ou encore à l'indépendance d'axiomes par rapport à ces systèmes. Le fil rouge de cette thèse est la construction de modèles syntaxiques, qui sont des modèles qui réutilisent la théorie des types pour interpréter la théorie des types. Dans une première partie, nous introduisons la théorie des types à l'aide d'un système minimal et de plusieurs extensions potentielles. Dans une seconde partie, nous introduisons les modèles syntaxiques donnés par traduction de programme et donnons plusieurs exemples. Dans une troisième partie, nous présentons Template-Coq, un plugin de métaprogrammation pour Coq. Nous montrons comment l'utiliser pour implémenter directement certains modèles syntaxiques. Enfin, dans une dernière partie, nous nous intéressons aux théories des types à deux égalités : une égalité stricte et une égalité univalente. Nous proposons une relecture des travaux de Coquand et. al. et Orton et Pitts sur le modèle cubique en introduisant la notion de fibrance dégénérée. / This thesis is about the metatheory of intuitionnistic type theory. The considered systems are variants of Martin-Löf type theory of Calculus of Constructions, and we are interested in the coherence of those systems and in the independence of axioms with respect to those systems. The common theme of this thesis is the construction of syntactic models, which are models reusing type theory to interpret type theory. In a first part, we introduce type theory by a minimal system and several possible extensions. In a second part, we introduce the syntactic models given by program translation and give several examples. In a third part, we present Template-Coq, a plugin for metaprogramming in Coq. We demonstrate how to use it to implement directly some syntactic models. Last, we consider type theories with two equalities: one strict and one univalent. We propose a re-reading of works of Coquand et.al. and of Orton and Pitts on the cubical model by introducing degenerate fibrancy.

La modularité est un enjeu important en programmation, surtout quand on l’enrichit avec des preuves, comme dans les langages avec des types dépendants. Typer est un tel langage, et afin d’augmenter sa modularité et de lui ajouter un moyen de faire la surcharge d’opérateurs, on s’inspire d’Agda et Coq et on l’étend avec les arguments instances, qui généralisent les classes de types de Haskell. Un aspect qui distingue notre conception est que comme Typer généralise les définitions, la généralisation des contraintes de classe est grandement facilitée. Pour pouvoir faire les preuves de lois de classes, on doit également ajouter l’élimination dépendante des types inductifs au langage, dont certains aspects sont en retour facilités par les arguments instances. Sur la base de ces deux fonctionnalités, on offre également une solution au problème de la cécité booléenne, tel que décrit par Harper. / Modularity is an important concern for software development, especially when the latter is enriched with proofs in a language with dependent types. Typer is such a language, and in order to increase its modularity, and also provide a way to overload operators, we take inspiration from Agda and Coq and extend it with instance arguments, a generalization of Haskell’s type classes. An aspect that sets our design apart is that since Typer generalizes definitions, it greatly simplifies the generalization of class constraints. In order to allow writing proofs for class laws, we must also implement the dependent elimination of inductive types. In return, instance arguments facilitate some details of dependent elimination. Using both features, we suggest a solution to the problem of Boolean Blindness.

La thèse porte sur l'impact d'optimisations algorithmiques pour la synthèse automatique HLS pour ASIC. Ces optimisations algorithmiques sont des transformations de haut niveau, qui de part leur nature intrinsèque restent hors de porter des compilateurs modernes, même les plus optimisants. Le but est d'analyser l'impact des optimisations et transformations de haut niveau sur la surface, la consommation énergétique et la vitesse du circuit ASIC. Les trois algorithmes évalués sont les filtres non récursifs, les filtres récursifs et un algorithme de détection de mouvement. Sur chaque exemple, des gains ont été possibles en vitesse et/ou en surface et/ou en consommation. Le gain le plus spectaculaire est un facteur x12.6 de réduction de l'énergie tout en maitrisant la surface de synthèse et en respectant la contrainte d'exécution temps réel. Afin de mettre en perspective les résultats (consommation et vitesse), un benchmark supplémentaire a été réalisé sur un microprocesseur ST XP70 avec extension VECx, un processeur ARM Cortex avec extension Neon et un processeur Intel Penryn avec extensions SSE.

La thèse porte sur l'impact d'optimisations algorithmiques pour la synthèse automatique HLS pour ASIC. Ces optimisations algorithmiques sont des transformations de haut niveau, qui de part leur nature intrinsèque restent hors de porter des compilateurs modernes, même les plus optimisants. Le but est d'analyser l'impact des optimisations et transformations de haut niveau sur la surface, la consommation énergétique et la vitesse du circuit ASIC. Les trois algorithmes évalués sont les filtres non récursifs, les filtres récursifs et un algorithme de détection de mouvement. Sur chaque exemple, des gains ont été possibles en vitesse et/ou en surface et/ou en consommation. Le gain le plus spectaculaire est un facteur x12.6 de réduction de l'énergie tout en maitrisant la surface de synthèse et en respectant la contrainte d'exécution temps réel. Afin de mettre en perspective les résultats (consommation et vitesse), un benchmark supplémentaire a été réalisé sur un microprocesseur ST XP70 avec extension VECx, un processeur ARM Cortex avec extension Neon et un processeur Intel Penryn avec extensions SSE. / The thesis deals with the impact of algorithmic transforms for HLS synthesis for ASIC. These algorithmic transforms are high level transforms that are beyond the capabilities of modern optimizing compilers. The goal is to analyse the impact of the High level transforms on area execution time and energy consumption. Three algorithms have been analyzed: non recursive filters, recursive filter and a motion detection application. On each algorithm, the optimizations and transformations lead to speedups and area/surface gains. The most impressive gain in energy reduction is a factor x12.6, while the area remains constant and the execution time smaller than the real-time constraint. A benchmark has been done on SIMD general purpose processor to compare the impact of the high level transforms: ST XP70 microprocessor with VECx extension, ARM Cortex with Non extension and Intel Penryn with SSE extension.