Skip to Main content Skip to Navigation
Journal articles

Abstract Representation of Binders in OCaml using the Bindlib Library

Rodolphe Lepigre 1 Christophe Raffalli 2
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a dozen languages and proof assistants (including a new version of the logical framework Dedukti). Bindlib is optimised for fast substitution, and it supports variable renaming. Since the representation of binders is based on higher-order abstract syntax, variable capture cannot arise during substitution. As a consequence, variable names are not updated at substitution time. They can however be explicitly recomputed to avoid "visual capture" (i.e., distinct variables with the same apparent name) when a data structure is displayed.
Document type :
Journal articles
Complete list of metadata
Contributor : Rodolphe Lepigre Connect in order to contact the contributor
Submitted on : Monday, January 7, 2019 - 2:44:52 PM
Last modification on : Monday, October 11, 2021 - 10:16:57 AM

Links full text



Rodolphe Lepigre, Christophe Raffalli. Abstract Representation of Binders in OCaml using the Bindlib Library. Electronic Proceedings in Theoretical Computer Science, EPTCS, 2018, 274, pp.42-56. ⟨10.4204/EPTCS.274.4⟩. ⟨hal-01972050⟩



Record views