Nominal Automata with Name Deallocation

Simon Prucker, Stefan Milius, Lutz Schröder

Data words with binders formalize concurrently allocated memory. Most name-binding mechanisms in formal languages, such as the $\lambda$-calculus, adhere to properly nested scoping. In c…