The Bindlib library for OCaml

Bindlib is a library allowing the manipulation of data structures with bound variables. It is particularly useful when writing ASTs for programming languages, but also for manipulating terms of the λ-calculus or quantified formulas. In the internals, binders are represented using a form of higher-order abstract syntax (HOAS).

Ressources:

• Introductory paper
• Generated documentation

Projects using Bindlib:

• Lambdapi (implementation of Dedukti)
• PML₂ language
• SubML language
• PML
• The Catala language
• Many more small projects...

Dependencies

List of dependencies:

• OCaml (at least version 4.07.0),
• The Dune build system (at least version 2.7.0).

Installation

You can either pin the repository with opam or run the following.

make
make install

Contributors

Main contributors:

• Christophe Raffalli (@craff, author of the first version)
• Rodolphe Lepigre (@rlepigre)

The project received additional contributions from:

• Alain (@adelaett)
• Rémi Nollet (@rnollet)
• Qiancheng Fu (@qcfu-bu)