LIPIcs.CSL.2015.374.pdf
- Filesize: 0.5 MB
- 16 pages
Document
Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes
Authors
-
Part of:
Volume:
24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2015-09-07
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)
https://doi.org/10.4230/LIPIcs.CSL.2015.374
https://doi.org/10.4230/LIPIcs.CSL.2015.374
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.
Keywords
- nominal sets
- scope
- alpha equivalence
- dynamic sequences
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads