Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.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 3 mai, 10h30

                             -----------------
                             Nicolas Pouillard
                             -----------------

                                   INRIA

             ==================================================
             A fresh look at programming with names and binders
             ==================================================

Dans une grande quantité de programmes, allant des compilateurs aux systèmes
de preuves, il faut manipuler des structures avec des lieurs et des noms.  Le
problème semble anodin du point de vue de la programmation mais il est en fait
bien difficile de choisir une représentation des lieurs et des noms.  On peut
vouloir une représentation naturelle, expressive et efficace.  Plus importants
encore sont les programmes manipulant ces structures: peut-on en démontrer la
sûreté tout en conservant expressivité et naturel?

A wide range of computer programs, including compilers and theorem provers,
manipulate data structures that involve names and binding. However, the design
of programming idioms which allow performing these manipulations in a safe
and natural style has, to a large extent, remained elusive.

In this paper, we present a novel approach to the problem. Our proposal can be
viewed either as a programming language design or as a library: in fact, it is
currently implemented within Agda.  It provides a safe and expressive means of
programming with names and binders.  It is abstract enough to support multiple
concrete implementations: we present one in nominal style and one in de Bruijn
style.  We use logical relations to prove that ``well-typed programs do not
mix names with different scope''. We exhibit an adequate encoding of
Pitts-style nominal terms into our system.