Leaving the nest: Nominal techniques for variables with interleaving scopes

Jamie Gabbay, Dan R. Ghica, Daniela Petrisan

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

4 Citations (Scopus)
34 Downloads (Pure)

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.

Original languageEnglish
Title of host publication24th EACSL Annual Conference on Computer Science Logic
Subtitle of host publicationCSL 2015, September 7–10, 2015, Berlin, Germany
EditorsStephan Kreutzer
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages374-389
Number of pages16
ISBN (Print)978-3-939897-90-3
DOIs
Publication statusPublished - Sep 2015
Event24th EACSL Annual Conference on Computer Science Logic 2015 - Berlin, Germany
Duration: 7 Sep 201510 Sep 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Volume41
ISSN (Print)1868-8969

Conference

Conference24th EACSL Annual Conference on Computer Science Logic 2015
Abbreviated titleCSL 2015
CountryGermany
CityBerlin
Period7/09/1510/09/15

Keywords

  • Alpha equivalence
  • Dynamic sequences
  • Nominal sets
  • Scope

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Leaving the nest: Nominal techniques for variables with interleaving scopes'. Together they form a unique fingerprint.

  • Cite this

    Gabbay, J., Ghica, D. R., & Petrisan, D. (2015). Leaving the nest: Nominal techniques for variables with interleaving scopes. In S. Kreutzer (Ed.), 24th EACSL Annual Conference on Computer Science Logic: CSL 2015, September 7–10, 2015, Berlin, Germany (pp. 374-389). (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 41). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2015.374