Bindlib-2.1 library for binders under OCaml available

From: Christophe Raffalli (
Date: Sun Jan 18 1998 - 18:35:35 MET

Date: Sun, 18 Jan 1998 18:35:35 +0100
From: Christophe Raffalli <>
Subject: Bindlib-2.1 library for binders under OCaml available

I am please to announce the release 2.1 of the bindlib library for

This is a completely rewritten library with no more strange restrictions
and a wider variety of examples. Have a try !


  This is a library for the Objective-Caml (and NJSML if someone
  really wants a port) providing reasonable tools to write programs
  manipulating data structures with binders (like lambda-terms or
  quantified formulae). It is quite efficient and not too difficult
  to use (at least for me).

  I do not know of any available alternative to this package resulting
  in a code as small, and as efficient (both in memory and speed) !
  So give it a try !


It is available from my URL:

Or by ftp:

Christophe Raffalli
Laboratoire de Mathématiques, LAMA
Université de Savoie

Email: URL:

------- History -------

Version 2.1 January, 15th, 1998:

- added bind_val family of functions. - added is_closed and related functions.

- added bind_pair, bind_list and related modules

- more complex examples available.

- only an objective-caml version at the moment

Version 2.0 November, 21th, 1997 (not really distributed):

- complete rewriting (no more strange restrictions) !

- only an objective-caml version at the moment

Version 1.2 November, 15th, 1995:

- Provide an SML version.

- Correct a bug (this bug could only appear with the native Caml-Special-Light compiler).

- The function cumul-abs is not provided anymore (the library decide by itself how it should optimized abstraction).

- The price to pay: start_term can only be called while no other construction is already started. Another function local_start is provided to start a new construction of a term inside another.

Version 1.1, October, 17th, 1995:

- Correct a major bug: when more than one variable is bound outside of the current sequence of binding, then the version 1.0 does not work at all. This bug has now been corrected.

- The library now raises the exception "Binlib_error" instead of "Invalid_argument".

- The memory usage has been optimised to take in account binder which binds a variable with no occurrence. In the benchmark this is not visible, but other examples shows an improvement of a factor greater than 2 !

- The library only works for terms with less than 32768 free variables in each sub-term. An exception is raised if you use too many variables.

- The library has now been tested on a bigger scale and should be more reliable (I hope)

Version 1.0, September, 27th, 1995:

- first public version

This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:13 MET