2026-08-17T14:29:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5426 2024-03-06T10:36:26Z ddc:004 open_access

Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes Gabbay, Murdoch J. Ghica, Dan R. Petrisan, Daniela nominal sets scope alpha equivalence dynamic sequences 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Murdoch J. Gabbay and Dan R. Ghica and Daniela Petrisan 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.374 urn:nbn:de:0030-drops-54262 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.374 eng https://creativecommons.org/licenses/by/3.0/legalcode