Une approche unifiante pour programmer sûrement avec de la syntaxe du premier ordre contenant des lieurs

• Main Author: Pouillard, Nicolas
• Language: ENG
• Published: Université Paris-Diderot - Paris VII 2012
• Subjects: [INFO:INFO_PL] Computer Science/Programming Languages; noms; lieurs; méta-programmation; abstraction de noms; indices de De Bruijn
• Online Access: http://tel.archives-ouvertes.fr/tel-00759059; http://tel.archives-ouvertes.fr/docs/00/75/90/59/PDF/PhD-thesis-latest.pdf; http://tel.archives-ouvertes.fr/docs/00/75/90/59/ANNEX/phd-defense-slides-en.pdf; http://tel.archives-ouvertes.fr/docs/00/75/90/59/ANNEX/phd-defense-slides.pdf; http://tel.archives-ouvertes.fr/docs/00/75/90/59/ANNEX/posterDIGITEO-improved.pdf; http://tel.archives-ouvertes.fr/docs/00/75/90/59/ANNEX/PhD-thesis-latest-black-and-white.pdf

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.