Nominal techniques for variables with interleaving scopes

Add to your list(s) Download to your calendar using vCal

• Dan Ghica (Computer Science)
• Tuesday 28 April 2015, 12:00-13:00
• CS 217.

If you have a question about this talk, please contact Dan Ghica.

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. ⟨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.

(joint work with Jamie Gabbay and Daniela Petrisan)

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.