Hard life with weak binders

We introduce weak binders, a lightweight construct to deal with fresh names in
nominal calculi.
Weak binders do not define the scope of names as precisely as the standard
nu-binders, yet they enjoy strong semantic properties.
We provide them with a denotational semantics, an equational
theory, and a trace inclusion preorder.
Furthermore, we present a trace-preserving
mapping between weak binders and nu-binders.