De nouveaux outils pour calculer avec des inductifs en Coq

• Main Author: Boutillier, Pierre
• Language: fra
• Published: Université Paris-Diderot - Paris VII 2014
• Subjects: [INFO:INFO_PL] Computer Science/Programming Languages; [INFO:INFO_PL] Informatique/Langage de programmation; Coq (logiciel); Assistants de preuve; Langages de programmation > Sémantique; Induction (logique); filtrage
• Online Access: http://tel.archives-ouvertes.fr/tel-01054723; http://tel.archives-ouvertes.fr/docs/01/05/47/23/PDF/these_boutillier.pdf; http://tel.archives-ouvertes.fr/docs/01/05/47/23/ANNEX/soutenace_boutillier.pdf

En ajoutant au lambda-calcul des structures de données algébriques, des types dépendants et un système de modules, on obtient un langage de programmation avec peu de primitives mais une très grande expressivité. L'assistant de preuve Coq s'appuie sur un tel langage (le CIC) à la sémantique particulièrement claire. L'utilisateur n'écrit pas directement de programme en CIC car cela est ardu et fastidieux. Coq propose un environnement de programmation qui facilite la tâche en permettant d'écrire des programmes incrémentalement grâce à des constructions de haut niveau plus concises. Typiquement, les types dépendants imposent des contraintes fortes sur les données. Une analyse de cas peut n'avoir à traiter qu'un sous-ensemble des constructeurs d'un type algébrique, les autres étant impossibles par typage. Le type attendu dans chacun des cas varie en fonction du constructeur considéré. L'impossibilité de cas et les transformations de type doivent être explicitement écrites dans les termes de Coq. Pourtant, ce traitement est mécanisable et cette thèse décrit un algorithme pour réaliser cette automatisation. Par ailleurs, il est nécessaire à l'interaction avec l'utilisateur de calculer des programmes du CIC sans faire exploser la taille syntaxique de la forme réduite. Cette thèse présente une machine abstraite conçu dans ce but. Enfin, les points fixes permettent une manipulation aisée des structure de données récursives. En contrepartie, il faut s'assurer que leur exécution termine systématiquement. Cette question sensible fait l'objet du dernier chapitre de cette thèse.