Document Open Access Logo

Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

Authors Murdoch J. Gabbay, Dan R. Ghica, Daniela Petrisan

Thumbnail PDF


  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Author Details

Murdoch J. Gabbay
Dan R. Ghica
Daniela Petrisan

Cite AsGet BibTex

Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan. Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 374-389, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)


We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. <delta x M x>) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.
  • nominal sets
  • scope
  • alpha equivalence
  • dynamic sequences


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail