One area which has consistently thrown up challenges in computer science has been the treatment of names and binding. Names can represent variable symbols in inductive proofs on syntax, but they also feature when reasoning about memory locations, or semi-structured data with pointers, or message-passing in security protocols, and elsewhere. Propagation of names describes connectedness and information flow.

Nominal techniques are based on nominal sets, an relatively elementary extension of “ordinary” sets (i.e. collections of elements). For this reason, nominal techniques have been particularly good for developing relatively elementary extensions of first-order systems to handle names and binding.

I will briefly survey the “nominal” literature and then describe recent work with Gilles Dowek and Dominic Mulligan aimed at developing an extension of first-order logic with names and binding, which we call Permissive Nominal Logic. This preserves the flavour of first-order logic but (we believe) allows a particularly clean, simple, and intuitive representation of axioms and proofs involving names and binding.

See the associatedpaper.