We generalise nominal abstract syntax from statically-scoped binding to dynamically-scoped explicit binding. This means that the usual statically-scoped operation for name-binding (familiar as the λ in λa.M or the ∀ in ∀a.p(a)) is split into a pair of operators: an explicit name-creation bracket ⟨a, and an explicit name-destruction bracket a⟩. We call this syntax dynamic sequences and we consider a comprehensive suite of models in inductive, denotational, and categorical style.
The situation where binding splits in this manner is rather common, corresponding to ‘malloc' and 'free' in C but also to (for instance) file handlers and network sockets. In this paper, we consider specific applications to modelling resource management and pointer sequences in game semantics.
This is joint work with Jamie Gabbay, Daniela Petrisan and Bertram Wheen.