By David Turner and Glynn Winskel, from CSL 2009, available from Glynn Winskel’s website:
This paper investigates a methodology of using FM (Fraenkel-Mostowski) sets, and the ideas of nominal set theory, to adjoin name generation to a semantic theory. By developing a domain theory for concurrency within FM sets the domain theory inherits types and operations for name generation, essentially without disturbing its original higher-order features. The original domain theory had a metalanguage HOPLA (Higher Order Process Language) and accordingly this expands to a metalanguage, Nominal HOPLA, with name generation (closely related to an earlier language new-HOPLA). Nominal HOPLA possesses an operational and denotational semantics which are related via soundness and adequacy results, again carried out within FM sets.
