General Terms

Nominal rewriting extends first-order rewriting with Gabbay-Pitts abstractors: bound entities are explicitly named (rather than being nameless, as for de Bruijn indices) yet rewrit-ing respects α-conversion and can be directly implemented, thanks to the use of freshness contexts. In this paper we study two extensions to nominal rewriting. First we intro-duce a Nquantifier for modelling name generation. This al-lows us to model higher-order functions involving local state, and has also applications in concurrency theory. The second extension introduces new constraints in freshness contexts. This allows us to express strategies of reduction and has ap-plications in programming language design and implemen-tation. Finally, we study confluence properties of nominal rewriting and its extensions