I would like to announce the first release of dblib, a library that is supposed to help work with de Bruijn’s encoding of binding.

The library is fairly reusable, and I have used it so far in two large proofs of type soundness. Reusability is obtained in part via type classes, in part via tactics that happen to “just work” (hopefully). The user is requested to write a certain amount of boilerplate code, which I think remains tolerable.

The README file is here:

http://gallium.inria.fr/~fpottier/dblib/README

and the complete distribution is here:

http://gallium.inria.fr/~fpottier/dblib/dblib.tar.gz

There is no formal documentation, but the library itself is heavily commented, and there are four little demos (one of which is included below) that help get started.

Your feedback is welcome. Enjoy!

Demo