Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

Murdoch J Gabbay, Dan Ghica, Daniel Petrisan

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

4 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationProceedings of 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
EditorsStephan Kreutzer
PublisherSchloss Dagstuhl
Pages347-389
Volume41
ISBN (Print)9783939897903
DOIs
Publication statusPublished - 4 Sept 2015
Event24th EACSL Annual Conference on Computer Science Logic (CSL 2015) - Berlin, Germany
Duration: 7 Sept 201510 Sept 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
Volume41
ISSN (Print)1868-8969

Conference

Conference24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Country/TerritoryGermany
CityBerlin
Period7/09/1510/09/15

Keywords

  • nominal sets
  • scope
  • alpha equivalence
  • dynamic sequences

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