Résumé
Le troisième séminaire a continué l’exploration de la programmation avec types dépendants débutée au premier séminaire. L’orateur a identifié deux écueils majeurs pour programmer dans une théorie des types comme celle de Coq : la partialité et la non-terminaison, et a montré comment l’utilisation de types dépendants permet de rendre les fonctions totales et d’en démontrer la terminaison. Se pose cependant le problème du filtrage dépendant, c’est-à-dire l’analyse par cas sur ces types dépendants, qui est plus complexe que le filtrage non dépendant usuel.
