La théorie des types observationnelle (OTT) est une extension de la théorie des types dépendants conçue par Altenkirch et McBride dans les années 2000. L'idée centrale d'OTT est qu'en modifiant le concept d'égalité, il devient possible d'avoir des types quotients et des fonctions extensionnelles sans compromettre le caractère constructif de la théorie des types dépendants.
Lors de cet exposé, j'expliquerai comment combiner la théorie observationnelle d'Altenkirch et McBride avec le Calcul des Constructions, la théorie des types qui sous-tend l'assistant à la preuve Coq. En particulier, j'expliquerai comment caractériser l'égalité des types inductifs de Coq, et comment les éliminateurs des types indexés utilisent une règle de calcul délicate à intégrer à la théorie.
Si le temps le permet, j'en profiterai pour faire une démonstration de la branche expérimentale Coq-observationnel, et pour discuter d'avancées récentes dans la sémantique ensembliste de la théorie des types observationnelle.