Nominal Scott Domains

Andrew Pitts

The theory of nominal sets, introduced by the speaker and Jamie Gabbay about 12 years ago, provides a theory for structures involving names, based on the mathematics of permutation actions. It has been explored for its applications to logic, to (operational, denotational and game) semantics, to metaprogramming in functional and logic programming languages, to rewriting, to interactive theorem provers, and to (history dependent) automata. Recently, that last application has re-emerged in the research programme of Mikolaj Bojanczyk et al on languages and automata over infinite alphabets (LICS 2011, POPL 2012, ICALP 2012). A key concept underlying that research programme turns out to coincide with one introduced (for quite different purposes) by Glynn Winskel and David Turner in their work on "nominal domain theory for concurrency" (CSL 2009).

In this talk I will explain the connection and use it to develop a notion of Scott domain within nominal sets. The functionals for existential quantification over names and "definite description" over names turn out to be compact (in the sense appropriate for nominal Scott domains). Adding them, together with parallel-or, to a language for recursively defined higher-order functions with name-abstraction and locally scoped names, one obtains a full abstraction result for nominal Scott domains analogous to Plotkin's classic result about PCF and conventional Scott domains.