The eighth meeting of the Wessex Theory Seminar took place on Tuesday 13th July 2010 at the University of Bath. Talks were held in room 1E2.4 from 2pm.


14.00 Martin Hyland: Varieties of Algebraic Theories

14.45 Giuseppe Rosolini: Remarks on Realizability (slides)

15.30 Coffee Break

16.00 Pawel Sobocinski: Representing Petri-Net Interactions (slides)

16.45 Guy McCusker: Graph-style models of programming languages

17.30 Close.


Pino Rosolini

Remarks on Realizability (slides)

The full internal category on modest sets in the effective topos is sufficiently complete to provide an elementary model of polymorphism, i.e. one where type abstraction is interpreted as products over the collection of all types provided the semanticist is prepared to use intuitionistic set theory in place of standard set theory. But that internal category is not complete.

Thus Peter Freyd's remark that an internal complete category of a (Grothendieck) topos is posetal could still hold for any topos - without the parenthesized assumption.

We show that the 1-category reflection of the 2-category PGRPD of the effective topos consisting of those internal PER-enriched groupoids with a projective object of objects, with enriched functors and natural transformations, gives a topos with an internal non-posetal category which is complete. Since it is complete it provides, in particular, another elementary model of polymorphism, and we believe that that is also parametric.

Guy McCusker

Graph-style models of programming languages

Scott's Pw graph model is one of the simplest and oldest models of the lambda-calculus. Recently, some similar-looking models have emerged which are capable of handling more sophisticated features, including imperative constructs and fresh name generation. This talk gives an overview of these models and their properties, and investigates what algebraic structure is needed to make them work.

Pawel Sobocinski

Representing Petri-Net Interactions (slides)

We introduce a novel compositional algebra of Petri nets, as well as a stateful extension of the calculus of connectors. These two formalisms are shown to have the same expressive power. A paper is available from Pawel's home page


From Bath:

From Cambridge:

From Southampton:

From Swansea:

From Genoa (Italy):

From Kent: