To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 17/11/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 17 novembre, 10h30

                                -----------
                                Marc Pouzet
                                -----------

                                    LRI

                         =========================
                         Le compilateur MiniLustre
                         =========================

Dans cet exposé, je présenterai l'architecture d'un compilateur minimaliste
utilise dans le cadre du développement d'une chaine de compilation certifiée
en Coq d'un langage synchrone de type SCADE/Lustre.

Ce compilateur s'appuie sur une formalisation de la technique de génération de
code modulaire utilisée depuis 2000 dans le compilateur ReLuC conçu avec
Jean-Louis Colaço. ReLuC a servi de base au développement du nouveau
compilateur qualifié de SCADE 6.

Je montrerai l'utilisation des horloges pour obtenir du code séquentiel
raisonnablement efficace. Je discuterai de la mise en oeuvre de ce compilateur
en Coq et l'état actuel de ce développement.