Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Colleges, School and Institutes

External organisations

  • Heriot Watt Univ
  • Radboud Univ Nijmegen


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.


Original languageEnglish
Title of host publicationProceedings of 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
EditorsStephan Kreutzer
Publication statusPublished - 4 Sep 2015
Event24th EACSL Annual Conference on Computer Science Logic (CSL 2015) - Berlin, Germany
Duration: 7 Sep 201510 Sep 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
ISSN (Print)1868-8969


Conference24th EACSL Annual Conference on Computer Science Logic (CSL 2015)


  • nominal sets, scope, alpha equivalence, dynamic sequences