Tuesday 16 November 2017, 14:00, LSV: An introduction to Bindlib in the context of Dedukti, Rodolphe Lepigre (Deducteam).

The implementation of programming languages and/or of theorem provers plays an important role in our community. It has two main (non-exclusive) goals: it can be used to concretely illustrate the mathematical models that we consider, and it can also be used to discover new intuitions by experimenting with the code. In practice, implementing languages is more difficult than one could expect. A great deal of techniques need to be combined, from the parsing of source files to unification algorithms, through the representation of binding structures.

In this talk, I will focus on the latter point and introduce the Bindlib OCaml library, which allows for an efficient representation of binders (in terms of substitution speed) and supports variable renaming. In particular, I will show you how Bindlib is used in my new implementation of Dedukti.