On a monadic semantics for freshness

A standard monad of continuations, when constructed with domains in the world of FM-sets [M.J. Gabbay, A.M. Pitts, A new approach to abstract syntax with variable binding, Formal Aspects Comput. 13 (2002) 341-363], 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 “Fresh” series of metalanguages [M.R. Shinwell, Swapping the atom: Programming with binders in Fresh O'Caml, Proc. MERλIN, 2003; M.R. Shinwell, A.M. Pitts, Fresh O'Caml User Manual, Cambridge University Computer Laboratory, September 2003, available at 〈http://www.freshml.org/foc/〉; M.R. Shinwell, A.M. Pitts, M.J. Gabbay, FreshML: Programming with binders made simple, in: Proc. ICFP '03, ACM Press, 2003, pp. 263-274] respect α-equivalence of object-level languages up to meta-level contextual equivalence.