To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 01/06/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

                           Vendredi 1 juin, 10h30

                               --------------
                               Zaynah Dargaye
                               --------------

                                   INRIA

                        ============================
                        Transformation CPS certifiée
                        ============================

La transformation en style CPS est une passe courante dans la compilation des
langages fonctionnels. L'étude de la certification de cette transformation est
donc pertinente dans la réalisation d'un compilateur certifié pour miniML en
Coq. De tels travaux ont déjà été menés en Isabelle/HOL et Twelf.
  
Cette présentation résumera ces deux travaux, avant de décrire la
transformation CPS en Coq et les principaux éléments de sa preuve de
correction.