**VENUE**: Lecture Theatre B (Level 1), Oxford University C=
omputing Laboratory (OUCL), Wolfson Building, Parks Road, Oxford

12:00 Depart for lunch from the OUCL Reception

=202:00--2:40: Nathan Bowler (University of Cambridge)

2:45--3:25: Mart=
in Churchill (University of Bath)

3:30--4:00 **coffee break 4:00--4:40: James Laird (University of Bath) 4:40--5:40 **

From the Wessex Theory Seminar sites:

=20**Bath**: Martin Churchill, James Laird, Ana Martins

~~Cambridge: Nathan Bowler, Martin Hyland~~

**Queen Ma=
ry, University of London**: Paulo Oliva

**Oxford**:=
Christopher Broadbent, Matthew Hague, David Hopkins, Andrzej Murawski, Luk=
e Ong, Stephen Ramsay, Jamie Vicary

**Southampton**: Toby =
Wilkinson

**Swansea**: Ulrich Berger, Oliver Kullmann

In addition:

**Birmingham**: Dan Ghica

A common intuitive construction of categories of games encodes the basic= combinatorics involved in various approaches to the study of games, for ex= ample Conway's recursively structured theory, or the specialised theory of = hypergraph games. These ideas have provided some key examples of models of = (various fragments of) intuitionistic and linear logic. Such categories hav= e also been used to construct denotational semantics for various abstract p= rogramming languages, including the construction of a fully abstract model = for PCF.

=20I'll begin by outlining an example of such a category (based on bicolour= ed digraphs) which allows the incorporation of some of the structure of the= theory of hypergraph games. I'll explain how this construction points to t= he language of fc-multicategories as a natural setting for the development = of additional structure in categories of games. This language also provides= a new setting for the construction of existing categories of games. I'll i= llustrate how the constructions in this setting have a modular form, cleanl= y separating different aspects of the underlying combinatorics, and I'll sk= etch some possible applications to the development of new constructions.=20

Many logics and programming languages can be equipped with game

sema=
ntics, whereby programs of type A (or proofs of proposition A)

are repr=
esented by strategies over the game representation of A. In

the case of=
proof semantics, the strategies in question are

total. These games mod=
els often admit definability results =E2=80=94 for

a given system, we m=
ight provide some constraints on strategies such

that each strategy sat=
isfying said constraints is the denotation of

some program (or proof.) =
In this work we consider a relatively

constraint-free games model (in w=
hich one can embed many other games

models, albeit a finitary version).=
We develop a proof system for this

model that is ``fully complete'' in=
a strong sense: proofs of a

formula are in 1-1 correspondence with tot=
al strategies over the game

representation of that formula. Thus we can=
use the logic to represent

strategies syntactically, and thus use it t=
o model proofs in

Multiplicative Linear Logic, imperative objects, and =
so on. The logic

is polarised and contains many standard connectives (t=
ensors, with,

par, exponentials...) although the proof rules themselves=
are

nonstandard =E2=80=94 a key notion is that of a sequoid operator f=
rom Lai02,

identifying the location of the next move (or focus) of the =
formula.

We describe a setting in which rather simple and concrete games models f=
or

programming languages with higher-rank polymorphic types can be give=
n. It

is based on Hyland-Ong style games, in which languages with many<=
br> computational features have been interpreted, and related techniques fo=
r

model-checking them developed. In particular, we describe a model of =
a

language with polymorphism and general references which is fully abst=
ract,

and also effectively presentable.

Closed types in the model denote HO-style arenas with an additional enab=
ling

relation on moves. Open types denote endofunctors on these arenas =
which are

in essence "arenas with (explicit) holes", so that their acti=
on is given by

plugging arenas and strategies into this hole. These for=
m a (closed Freyd)

category, in which morphisms are natural transformat=
ions which play copycat

between the holes. Universal quantification plu=
gs the one-move arena into

each hole, and uses the new enabling structu=
re to specify the copycat

links. Proving full abstraction (and definabi=
lity of finitary strategies as

terms) is surprisingly simple based on a=
kind of "internal genericity"

property.