Variables underpin mathematics and logic, appearing in algebraic equations, integrals, and quantified formulas, to give three examples. In an algebraic equation, there is usually implicit universal quantification. The variables range over all (suitable) values. In the integral expression, and in quantified formulas, the variables will be bound by the quantifier or the integral symbol. More strictly, some of the variables will be bound, and others free. A problem occurs when we substitute an expression for a free variable. Some of the free variables in the expression may become captured by the binding construct (that is, a quantifier or integral), and it is folklore in the lambda calculus community that the first published definition of formal substitution was incorrect.

This might be an interesting intellectual curiosity, except for the fact that the representation of variables in computer systems, such as theorem provers, inherits these problems. One way out is to use “nameless dummies” for variables, an approach pioneered by de Bruijn; while this notation is perfectly good for machines, it is horrible to read. So there is a question of how to devise a practical canonical system for dealing with variables, and one answer is provided by this paper, which also presents a brief review of some of the authors’ previous work, as well as nominal approaches pioneered by Pitts.

The authors’ system is based on using distinct syntactic classes for bound variables and free variables, an approach that was first used by Frege in his formulation of formal logic. The work in the paper builds on earlier work, but takes a more abstract view. It is shown that the approach gives a representation isomorphic with the nominal approach implemented in Isabelle, and indeed the meta-theoretical results are formally proved in Isabelle (and the proof scripts are available for download).

This is a well-written paper that presents a new solution to a long-standing problem and places that work squarely in context. It will be of value to the growing community of those involved in formalizing systems meta-theory, as well as to implementers of logics and other formal systems.