PPLV Seminar: Alpha equivalence for interleaved scopes

Speaker: Dr Dan Ghica, Reader in the School of Computer Science, University of Birmingham
UCL Contact: Reuben Rowe (Visitors from outside UCL please email in advance).
Date/Time: 10 Feb 16, 16:00 - 17:00
Venue: 1.02

Abstract

I will describe 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 which admit interleaving. We will see an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. I will sketch some potential applications to semantics of programming languages with explicit resource allocation and release. This is joint work with James Gabbay and Daniela Petrisan.