Sites Inria

English version

Séminaire des équipes de recherce

Abstract Representation of Binders using the Bindlib Library

© INRIA Sophie Auvin - G comme Grille

The Bindlib library provides a set of tools for the manipulation of structureswith 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

  • Date : 1/10/2018
  • Lieu : Inria de Paris - 2 rue Simone Iff 75012 - Batiment C - Salle Lions 1
  • Intervenant(s) : Rodolphe Lepigre

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.

Mots-clés : Séminaire Gallium Inria de Paris

Haut de page

Suivez Inria