Sites Inria

English version

Soutenance de thèse

De nouveaux outils pour calculer avec les inductifs en Coq

Pierre BOUTILLIER ( PIR2 )

  • Date : 18/02/2014
  • Lieu : Salle des thèse de l'Université Paris Diderot - 10 rue Françoise Dolto 75013 Paris - Accès Halle aux farines Hall F, 5ème étage - 14h30

En ajoutant au λ-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 CCI) à la sémantique particulièrement claire. L'utilisateur n'écrit pas directement de programme en CCI 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 du CCI. Pourtant, ce traitement est mécanisable et cette thèse décrit un algorithme pour réaliser cette automatisation.

Du point de vue du retour d'information de la part du système, 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.

Jury :

M.Yves Bertot : rapporteur
M.Roberto Di Cosmo : président
M.Hugo Herbelin : directeur
M.Daniel Hirschkoff : examinateur
M.Conor McBride : examinateur
Mme.Christine Paulin-Mohring : examinatrice
M.Carsten Schuermann : rapporteur

Mots-clés : Soutenance de thèse Coq Nouveaux outils PIR2 Paris

Haut de page

Suivez Inria