It is remarkable how apparently simple ideas can be difficult to formalize. A bound variable--a variable that has a scope, such as the body of the function for which it is a parameter--is a case in point. When the lambda calculus was emerging in the 1930s and 1940s, more than one of the pioneers tripped up defining precisely how one expression could be substituted for a variable, without the structure of the bound variables changing, and “capture” perhaps taking place. This was, of course, resolved in time, but it’s interesting to observe that even now, mathematicians will use informal strategies, such as the Barendregt convention, to deal with bound variables in practice.

So, it should be perhaps less of a surprise to learn that dealing with variable binding inside computer systems using formal languages--such as the interactive theorem provers Isabelle, HOL, and Coq--is by no means straightforward. There are two general approaches. The first represents variables as objects of the metalanguage (the language in which the logic is formalized). This can be done by using strings, numbers (or de Bruijn indices), or other more complex approaches; each requires users to think explicitly about variable names--there’s no Barendregt convention inside a theorem prover! The other approach is to identify the variables to be modeled with variables in the metalanguage; it is to this tradition that this paper belongs.

Without going into detail, this approach works by identifying functions with bound variables as a new kind of function in the metalanguage. These are functions that--following the definition of Reynolds--are parametric, which in this case means that they purely construct values, without analyzing their inputs. This construction can then support the construction of least-fixed points to model recursive type definitions, a sticking point of previous approaches.

While deeply technical, the paper is very clearly written and the introduction provides a very clear summary of the various syntactic approaches, as well as the motivation for the work that it introduces.