License:
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.374
URN: urn:nbn:de:0030-drops-54262
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5426/
Gabbay, Murdoch J. ;
Ghica, Dan R. ;
Petrisan, Daniela
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. 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 |
Collection: |
|
24th EACSL Annual Conference on Computer Science Logic (CSL 2015) |
Issue Date: |
|
2015 |
Date of publication: |
|
07.09.2015 |