To: seminaire@pauillac.inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 26/01/07 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/subscribe.html S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Salle de réunion du bâtiment 5 Vendredi 26 janvier, 10h30 -------------- Zaynah Dargaye -------------- INRIA ========================= Décurryfication certifiée ========================= La décurryfication (transformation de fonctions curryfiées en fonctions n-aires) est une optimisation courante dans la compilation des langages fonctionnels. Nous présentons ici une preuve de préservation sémantique de cette optimisation menée dans l'assistant de preuve Coq. Cet effort s'inscrit dans la réalisation d'un compilateur certifié pour miniML purement fonctionnel.