Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Salle de conférences du bâtiment 7 Lundi 16 mai, 10h30 ------------ Bruno Barras ------------ INRIA ====================================== Formalisation d'un modèle ensembliste du Calcul des Constructions Inductives ====================================== Avoir un modèle du formalisme de Coq (le CCI) est un objectif important. Outre une indication significative de l'absence de contradiction dans la logique employée, cela permet de justifier l'emploi de certains axiomes (extensionnalité, choix, etc.), ce qui a déjà pu être un problème par le passé. On s'intéresse ici aux modèles ensemblistes (les constructions sont interprétées par des objets de la théorie des ensembles) et extensionnels, qui permettent de justifier la plupart des axiomes employés couramment par les mathématiciens "standards". Bien que relativement intuitive, la construction détaillée d'un modèle pour un calcul aussi complexe que le CCI est assez technique et la littérature est souvent assez évasive, voire omet de mentionner certaines difficultés. C'est pourquoi nous avons choisi de faire cette modélisation en Coq, transformé à l'occasion en prouveur pour la logique de Zermelo Fraenkel intuitionniste (IZF). Dans cet exposé, plus que sur la construction détaillée, on se concentrera surtout sur la méthode de modélisation employée, applicable à une très large famille de théories des types, et sur le sens que l'on peut donner à un modèle de Coq exprimé en théorie des ensembles, elle-même encodée en Coq. (Veuillez noter la salle inhabituelle -- bâtiment 7.)