To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 18/02/08 - 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 Amphi Turing du bâtiment 1 Lundi 18 février, 10h30 ---------------- Alexandre Miquel ---------------- Université Paris 7 ================================================================== Extraction de programme classique dans le Calcul des Constructions ================================================================== Dans cet exposé, je me propose de montrer que les techniques de réalisabilité classique introduites par Jean-Louis Krivine sont compatibles avec le Calcul des Constructions avec univers (CCw), et qu'elles permettent d'envisager un mécanisme d'extraction de programme à partir de preuves classiques (avec proof-irrelevance et axiome du choix) formalisées en Coq (dans la sorte Prop). Pour cela, je commencerai par rappeler ce qu'est la réalisabilité classique au sens de Krivine (langage et modèles). Ensuite je montrerai comment étendre le modèle de réalisabilité de Krivine (initialement défini pour l'arithmétique du second ordre) à CCw, en utilisant une structure de Pi-set réminiscente des structures de omega-set (Hyland, Longo, Moggi), de D-set (Streicher) et de lambda-set (Altenkirch). Enfin, je présenterai un certain nombre de pistes pour étendre ce schéma d'extraction aux types inductifs (notamment les entiers) en utilisant des structures de données efficaces dans le langage cible (entiers binaires).