Generalised Name Abstraction for Nominal Sets
Ranald Clouston (ANU)
LOGIC AND COMPUTATION SEMINARDATE: 2012-04-24
TIME: 15:30:00 - 16:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
The Gabbay-Pitts nominal sets model is an elegant and popular framework for reasoning with names in abstract syntax. It has appealing semantics for name binding, via a functor mapping each nominal set to the 'atom-abstractions' of its elements. We wish to generalise this construction for applications where sets, lists, or other patterns of names are bound simultaneously. The atom-abstraction functor has left and right adjoint functors that can themselves be generalised, and their generalisations remain adjoints, but the atom-abstraction functor in the middle comes apart to leave us with two notions of generalised abstraction for nominal sets.
