To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 27/03/07 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Salle de réunion du bâtiment 5 Mardi 27 mars, 10h30 ---------------- Alexandre Miquel ---------------- Université Paris 7 ======================================================== Sémantiques dénotationnelles du calcul des constructions ======================================================== Dans cet exposé, je ferai un tour d'horizon des différents modèles (standard et moins standard) du calcul des constructions, le formalisme sous-jacent au système Coq. La première partie de l'exposé sera consacrée au modèle ensembliste "classique" du calcul des constructions, dans lequel tous les termes de preuve sont identifiés (la "proof-irrelevance"). J'y introduirai notamment les outils nécessaires pour interpréter les univers prédicatifs (Type_i), et évoquerai les problèmes posés par l'interprétation de la cumulativité Prop/Type. Dans la seconde partie de l'exposé, je montrerai comment certaines extensions du formalisme apparemment inoffensives conduisent à introduire des modèles plus sophistiqués tels que le modèle basé sur la réalisabilité et les omega-sets, ou le modèle construit dans les espaces cohérents.