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 - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                            Lundi 1 octobre, 10h30

                               ----------------
                               Rodolphe Lepigre
                               ----------------

                  Inria, LSV, CNRS, Université Paris-Saclay

         ============================================================
         Abstract Representation of Binders using the Bindlib Library
         ============================================================

The Bindlib library provides a set of tools for the manipulation of structures
with variable binding. It is very well suited for the representation of syntax
trees, and has already been used for the implementation of several programming
languages and proof assistants (including a new version of the Dedukti logical
framework). Bindlib is optimised for fast substitution,  and supports variable
renaming.  Since binders are represented using a form of higher-order abstract
syntax,  variable capture cannot arise during substitution.  As a consequence,
variable names are not updated at substitution time.  They can nonetheless  be
explicitly recomputed to avoid “visual capture” (i.e., distinct variables with
the same apparent name) when a data structure is displayed.

This is joint work with Christophe Raffalli.