Sémantiques dénotationelles du Calcul des Constructions

Alexandre Miquel

Projet LogiCal -- INRIA Rocquencourt

Abstract:
Dans cet exposé, nous présentons un certain nombre de modèles standard du Calcul des Constructions, le formalisme sous-jacent au système Coq.

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.


Marieke Huisman
Last modified: Tue Nov 21 13:12:44 MET 2000