Dans une première partie, nous effectuerons la construction du modèle ensembliste du Calcul des Constructions dans lequel tous les termes de preuve sont identifiés (modèle classique, ou "proof-irrelevant"), lequel permet d'établir la cohérence logique du formalisme.
Ensuite, nous introduirons un certain nombre d'outils supplémentaires afin d'interpréter les univers prédicatifs (Type_i) ainsi que la sorte calculatoire (Set) à partir de laquelle est réalisée l'extraction de programmes dans Coq.
Dans une troisième partie, nous évoquerons des travaux plus récents basés sur la théorie des domaines (espaces cohérents), lesquels suggè่rent l'ajout de constructions telles que les types intersection ou le sous-typage dans la syntaxe du Calcul des Constructions.
Nous pourrons alors conclure en remarquant que la sémantique déotationnelle --- introduite à l'origine pour prouver la cohérence (relative) de formalismes riches et expressifs --- est également une source d'inspiration précieuse qui suggère naturellement de nombreuses extensions à la syntaxe des formalismes étudiés.
Slides of this talk
Back to schedule.