a1 School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, Scotland
Nominal sets are a sets-based first-order denotation for variables in logic and programming. In this paper we extend nominal sets to two-level nominal sets. These preserve much of the behaviour of nominal sets, including notions of variable and abstraction, but they include a denotation for both variables and meta-variables. Meta-variables are interpreted as infinite lists of distinct variable symbols. We use two-level sets to define, amongst other things, a denotation for meta-variable abstraction, and nominal style datatypes of syntax-with-binding with meta-variables. We discuss the connections between this and nominal terms and prove a soundness result.
(Received August 01 2010)
(Revised February 07 2011)
(Online publication May 27 2011)