Cette thèse décrit une nouvelle approche pour la méta-programmation sûre. Un méta-programme est un programme qui manipule des programmes ou assimilés. Les compilateurs et systèmes de preuves sont de bons exemples de méta-programmes qui bénéficieraient de cette approche. Dans ce but, ce travail se concentre sur la représentation des noms et des lieurs dans les structures de données. Les erreurs de programmation étant courantes avec les techniques usuelles, nous proposons une interface abstraite pour les noms et les lieurs qui élimine ces erreurs. Cette interface est implémentée sous forme d'une bibliothèque en Agda. Elle permet de définir et manipuler des représentations de termes dans le style nominal. Grâce à l'abstraction, d'autres styles sont aussi disponibles : le style de De Bruijn, les combinaisons de ces styles, et d'autres encore. Nous indiçons les noms et les termes par des mondes. Les mondes sont en même temps précis et abstraits. Via les relations logiques et la paramétricité, nous pouvons démontrer dans quel sens notre bibliothèque est sûre, et obtenir des "théorèmes gratuits" à propos des fonctions monde-polymorphiques. Ainsi une fonction monde-polymorphique de transformation de termes doit commuter avec n'importe quel renommage des variables libres. La preuve est entièrement conduite en Agda. Notre technique se montre utile sur plusieurs exemples, dont la normalisation par évaluation qui est connue pour être un défi. Nous montrons que notre approche indicée par des mondes permet d'exprimer un large panel de type de données grâce a des langages de définition embarqués.

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage. / In computer science, structures with variable binders are very common. Program- ming languages and logical frameworks are examples of structures with binders. Thus writing programs that deal with these kinds of data benefits with explicit support for data binding. The Beluga programming environment is an example of such a system. In this work we develop and present a compiler for the system. Many of the programs that Beluga is specially well suited for writing can benefit from a compiler. For example, some of the kinds programs that would benefit more are type-checkers, compilers and interpreters that take advantage of the binder support and dependent types present in the language, and also require a reasonably fast run-time. Our goal in this work, is to present a compiler for the Beluga system, that uses a very versatile internal representation that helps with the development of the system, and allows a sharing of code between several back-ends. Furthermore, we present a way of compiling the uniquely powerful pattern language supported by Beluga.

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage. / In computer science, structures with variable binders are very common. Program- ming languages and logical frameworks are examples of structures with binders. Thus writing programs that deal with these kinds of data benefits with explicit support for data binding. The Beluga programming environment is an example of such a system. In this work we develop and present a compiler for the system. Many of the programs that Beluga is specially well suited for writing can benefit from a compiler. For example, some of the kinds programs that would benefit more are type-checkers, compilers and interpreters that take advantage of the binder support and dependent types present in the language, and also require a reasonably fast run-time. Our goal in this work, is to present a compiler for the Beluga system, that uses a very versatile internal representation that helps with the development of the system, and allows a sharing of code between several back-ends. Furthermore, we present a way of compiling the uniquely powerful pattern language supported by Beluga.