On a Monadic Semantics for Freshness
A standard monad of continuations, when constructed with domains
in the world of FM-sets,
is shown to provide a model of dynamic allocation of fresh names
that is both simple and useful. In particular, it is used to
prove that the powerful facilities for manipulating fresh names
and binding operations provided by the "FreshML" series of
metalanguages [www.freshml.org] respect
alpha-equivalence of object-level languages up to meta-level
contextual equivalence.