Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Gabbay, Murdoch J.; Ghica, Dan R.; Petrisan, Daniela http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-54262
URL:

; ;

Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

pdf-format:


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. 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.

BibTeX - Entry

@InProceedings{gabbay_et_al:LIPIcs:2015:5426,
  author =	{Murdoch J. Gabbay and Dan R. Ghica and Daniela Petrisan},
  title =	{{Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{374--389},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5426},
  URN =		{urn:nbn:de:0030-drops-54262},
  doi =		{10.4230/LIPIcs.CSL.2015.374},
  annote =	{Keywords: nominal sets, scope, alpha equivalence, dynamic sequences}
}

Keywords: nominal sets, scope, alpha equivalence, dynamic sequences
Seminar: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue date: 2015
Date of publication: 2015


DROPS-Home | Fulltext Search | Imprint Published by LZI