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.