TypiCal

Intervenant: Bruno Barras

Date et lieu: Jeudi 7 mai 2009, 14h00-16h00, salle de conférence du LIX

Résumé: La première partie de mon exposé fera des rappels au sujet du Calcul des Constructions Implicites (ICC). En particulier, je montrerai en quoi ICC est beaucoup plus souple que Coq en matière de spécification de programmes. Après ces rappels, je dresserai la stratégie pour étendre ce formalisme avec des types inductifs, dont un prototype est déjà implanté.

La première extension concerne l'égalité. Celle-ci est assez facile car le modèle de ICC d'Alexandre Miquel permet déjà de la justifier. Au passage je montrerai comment ajouter l'axiome K de Streicher (qui permet d'implanter le filtrage a la Epigram/Agda) à Coq en seulement 4 caractères.

L'extension de ICC avec des Sigma-types (paires dépendantes) sera plus difficile, si l'on inclut la notion (nouvelle) de Sigma-type implicite où l'une des 2 composantes de la paire est implicite. Suivant la composante considérée implicite, on introduit les notions de sous-type ou d'union de type. Si la métathéorie syntaxique ne pose pas de problème, le modèle d'espaces cohérents d'Alexandre n'est pas stable par union: l'union de types sémantiques n'est pas un type sémantique.

Récemment, Alexandre a prouvé qu'il était possible de "compléter" une union de types sémantiques en un type sémantique, et que cela justifie notre extension. Cette complétion a pour effet inattendu de fusionner certains éléments qui étaient distincts dans leur type d'origine. Pour mettre en évidence ce phénomène et expliquer en quoi cela est finalement intuitif, je présenterai de manière minimaliste le modèle d'Alexandre basé sur les espaces cohérents.