To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 06/04/09 - 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 6 avril, 10h30 --------------- Stéphane Glondu --------------- PPS, Université Paris 7 ====================================================== Coq : extraction certifiée ou certification extraite ? ====================================================== L'assistant de preuves Coq permet la génération de programmes corrects par construction. Cette fonctionnalité, appelée extraction, est de plus en plus exploitée pour produire des bibliothèques de fonctions certifiées, voire des programmes tout entier. Ainsi, un compilateur d'un sous-langage du C a été développé avec Coq, et un compilateur pour langage fonctionnel est en cours. Cependant, l'extraction elle-même n'est pas certifiée. Dans cet exposé, je présenterai deux approches pour certifier l'extraction : l'extraction certifiée, et la certification extraite.