@inproceedings{15f97344820d4c2e836e0ffc6704f5e2,
title = "Leaving the nest: Nominal techniques for variables with interleaving scopes",
abstract = "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. λx.M) is handled by explicit name-creation and name-destruction brackets (e.g. 〈xMx〉) 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 some preliminary applications to game semantics.",
keywords = "Alpha equivalence, Dynamic sequences, Nominal sets, Scope",
author = "Jamie Gabbay and Ghica, {Dan R.} and Daniela Petrisan",
year = "2015",
month = sep,
doi = "10.4230/LIPIcs.CSL.2015.374",
language = "English",
isbn = "978-3-939897-90-3",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
pages = "374--389",
editor = "Stephan Kreutzer",
booktitle = "24th EACSL Annual Conference on Computer Science Logic",
note = "24th EACSL Annual Conference on Computer Science Logic 2015, CSL 2015 ; Conference date: 07-09-2015 Through 10-09-2015",
}