Brian Aydemir, Stephanie Weirich, and Steve Zdancewic
Abstract: Binding is a fundamental part of language specification, yet it is both difficult and tedious to get right. In previous work, we argued that an approach based on locally nameless representation and cofinite quantification can provide a portable, transparent, lightweight methodology to define the semantics of binding. Although the binding infrastructure required by this approach is straightforward to develop, it can grow quadratically with the number of sorts of variables in the object language.
In this paper, we critically compare a spectrum of approaches that attempt to ameliorate this tedium by unifying the treatment of variables and binding. In particular, we compare our original methodology with two alternative ideas: First, we use a variant of higher-order abstract syntax (HOAS) to define variable binding in the object language via variable binding in a reusable meta-language. Second, we present a novel approach that collapses the syntactic categories of the object language together, permitting variables to be shared between them.
Our main contribution is a careful characterization of the benefits and drawbacks of each of approach. In particular, we use the multiple solutions to the POPLmark challenge in the Coq proof assistant to point out specific consequences with respect to the size of the binding infrastructure, transparency of the definitions, impact to the metatheory of the object language, and adequacy of the object language encoding.