To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Gallium - 14/09/06 - 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 conférence du Bat 8

                         Jeudi 14 septembre, 10h30

                             ------------------
                             Arthur Charguéraud
                             ------------------

                          ENS Lyon + Étudiant MPRI

          =======================================================
          Proofs with Binders - Working on the POPLMark Challenge
          =======================================================


  POPLMark Challenge aims at comparing ways of formalizing the Metatheory of
  Programming  Languages. During  the  5  months of  our  internship at  the
  University  of Pennsylvania  working  with Benjamin  Pierce and  Stephanie
  Weirich,  we analysed,  engineered and  compared different  techniques for
  solving that  Challenge. As  an outcome of  the comparison, we  designed a
  solution which we argue is a  good step towards the goal of the Challenge:
  the proofs it contains are  rather short and intuitive, and the technology
  used is  transparent and accessible (formalization in  Coq).  Our solution
  is  based on  a  locally  nameless representation  of  terms, where  bound
  variables are  represented using de-Bruijn indices and  free variables are
  given names (a technique previously experimented by Xavier Leroy).  In our
  presentation, we  will present the  conclusions of our  comparison between
  the different ways  of representing binders, give all  the key features of
  our  solution, and explain  briefly how  we implemented  the corresponding
  definition and proofs in Coq.