Nominal Equational Logic
This paper studies the notion of "freshness" that often occurs in
the metatheory of computer science languages involving various kinds
of names. Nominal Equational Logic is an extension of ordinary
equational logic with assertions about the freshness of names. It is
shown to be both sound and complete for the support interpretation
of freshness and equality provided by the Gabbay-Pitts nominal sets
model of names, binding and α-conversion.