Binding Operators for Nominal Sets

The theory of nominal sets is a rich mathematical framework for studying syntax and variable binding. Within it, we can describe several binding disciplines and derive convenient reasoning principles that respect α-equivalence. In this article, we introduce the notion of binding operator, a novel construction on nominal sets that unifies and generalizes many forms of binding proposed in the literature. We present general results about these operators, including sufficient conditions for validly using them in inductive definitions of nominal sets.