To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 12/10/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
                         Amphi Turing du bâtiment 1

                         Vendredi 12 octobre, 10h30

                              ---------------
                              Benjamin Werner
                              ---------------

                                   INRIA

                ===========================================
                Normalisation par Evaluation et HOAS en Coq
                ===========================================

Le lambda-calcul simplement typé peut être plongé en théorie des types (et
donc en Coq) de deux manières. D'une part, c'est un fragment de la théorie des
types. Par exemple l'identité existe en Coq: fun x => x; c'est ce qu'on
appelle parfois le plongement superficiel (shallow). D'autre part, on peut
construire un type de données pour représenter les lambda-termes et définir
ensuite le jugement de typage; c'est le plongement profond (deep).

Il est possible de construire les fonctions Coq qui passent d'un codage à
l'autre; ce sont essentiellement des fonctions de compilation et de
décompilation. La seconde correspond à ce que l'on appelle souvent la
Normalisation par Evaluation (NbE).

Je décrirai une implémentation particulière, où l'on privilégie la simplicité
du typage et le traitement des variables libres par rapport à la rapidité
d'exécution.

J'essayerai ensuite de montrer comment on pourrait utiliser ce travail pour un
nouveau traitement des langages avec lieurs (en s'inspirant de la syntaxe
abstraite d'ordre supérieur).