Many uses of names in programming languages and logical calculi are "atomic", in the sense that the structure of a name is immaterial: all that matters are distinctions between names and the association of names to the things named. In this talk I will give a gentle introduction to the topos of "nominal sets", a mathematical framework with names as atoms that can express the crucial property of "freshness" of names in a syntax-independent way. There are simple constructions on nominal sets for exponentiation, for name-abstraction and for name-restriction that illuminate the relationship between these notions and that of dynamic allocation of names in operational semantics. The category-theoretic characterisation and properties of name-abstraction and name-restriction hint at a categorical algebra for "equations modulo freshness constraints" that has yet to be investigated.

I shall discuss how Jamey Leifer, Ole Hoegh Jensen and I have set up the mathematical model of bigraphs, and where categorical ideas are useful. Bigraphs represent the dynamics of reconfigurable systems; their nodes can be nested and their edges don't have to respect the nesting (hence "bi"). They generalise process calculi (pi calculus, ambients, ...), and they can also model concrete "informatic" systems like people walking in and out of buildings carrying hand-held devices, plugging them into computers, and being detected (with benevolent intent) by sensors.
For modelling process calculi, including transition systems and bisimilarity, relative pushouts (RPOs) have provided a uniform basis. This is set up using s-categories, a well-behaved kind of precategory which allows one to keep track of the identity of graphical entities. Within this frame we recover already-known behavioural theories of processes.
Sorting is used to ensure that we get surjective (no junk) translations of processes. The forgetful functor that discards sorts must create RPOs if we are to use the behavioural theory; there are nice sufficient conditions for a functor to have this property, and these condtiions are satisfied by very useful sorting disciplines, including one that represents binding and scoping on names.
The aim of the talk is to expose these ideas to category theorists and receive comments and criticism in exchange.

The notion of innocent strategy as currently understood was one component in a games model for PCF, and has become an established part of game semantics. However the noton has seemed ad hoc to many and honest proofs of its properties can seem fiddly. In this work we describe a categorical context allowing a rational reconstruction of innocent and other similar strategies.

About 2 years ago Jim Laird has introduced a new kind of domains providing a fully abstract model for SPCF (i.e. PCF + catch) with non-recuperable errors. One can show that Laird domains provide a universal model for infinitary SPCF (i.e. with infinite terms). This has already been shown by J.Laird. But we give a simpler proof of this fact by showing that already type 1 over the natural numbers is universal for Laird domains. SPCF hosts the recursive type which provides a model for infinitary CPS target language (sort of an infinitary lambda-calculus). It can be shown that every term of SPCF can be ``realized'' by an object of D that can be denoted by a term of the infinitary CPS language. From this it follows that every object of D appears as denotation of an appropriate term of infinitary CPS, i.e. that D is a universal model. However, the model is not ``fully complete'' because different infinite normal forms receive the same interpretation in D. This suggests that -calculus is not the optimal representation of sequential algorithms or, rather, that the model D might give rise to an optimizing translation. This is joint work with my student Tobias Löw.

We will present, for non combinatorialists, the basic combinatorial motivations behind the development of the notion of Species of Structures and show why one should also consider variants of the notion. This will lead to consider Hopf algebra like structures on categories. we will illustrate with many examples.