sem2009/abstracts/herbelin

Sur quelques problèmes ouverts de la théorie de Coq et leurs conséquences pratiques

Hugo Herbelin INRIA et PPS

Le Calcul des Constructions Inductives (CCI), que l'on peut définir comme l'extension du Calcul des Constructions avec types inductifs que Coq implémente, est à la fois un langage de programmation fortement typé de fonctions terminantes et une logique de force comparable à celle de la théorie des ensembles.

Le CCI est un formalisme jeune qui continue d'évoluer (citons par exemple, l'abandon de l'imprédicativité des types lors du passage à la version 8.0 de Coq). L'objectif de cet exposé est de présenter un éventail de quelques questions ouvertes et limitations du CCI dans sa version actuelle.

Du côté de l'expressivité calculatoire, nous parlerons du manque de modularité des critères permettant de garantir la terminaison des fonctions et des conséquences de l'absence de validation de éta dans la théorie. En considérant le problème de la terminaison et celui des conditions de bord du filtrage dépendant, nous poserons aussi la question du compromis à trouver entre écriture naturelle de programme à types dépendants, ce qui nécessiterait de raffiner en la complexifiant la théorie sous-jacente, et encodage technique, ce que permet déjà la théorie actuelle, plus simple à décrire mais plus rigide à utiliser.

Du côté des aspects logiques, nous parlerons des problèmes que le sous-typage pose pour valider le modèle ensembliste du CCI ainsi que de la difficulté à marier raisonnement équationnel et annotations des types par des propriétés (c.-à-d. égalité extensionnelle et type dépendants). Nous évoquerons aussi les problèmes posés par les types dépendants pour faire fonctionner les « coupures commutatives » et le phénomène original de coupure dépendante que la présentation du CCI en calcul des séquents fait apparaître.