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.
Programme
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 PetriNet Interactions (slides)
16.45 Guy McCusker: Graphstyle models of programming languages
17.30 Close.
Abstracts
Anchor  


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 1category reflection of the 2category PGRPD of the effective topos consisting of those internal PERenriched groupoids with a projective object of objects, with enriched functors and natural transformations, gives a topos with an internal nonposetal 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.
Anchor  


Guy McCusker
Graphstyle models of programming languages
Scott's Pw graph model is one of the simplest and oldest models of the lambdacalculus. Recently, some similarlooking 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.
Anchor  


Pawel Sobocinski
Representing PetriNet 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
Attendance
From Bath:
 Ana C. Calderon
 Martin Churchill
 Guy McCusker
 John Power
From Cambridge:
 Nathan Bowler
 Martin Hyland
From Southampton:
 Julian Rathke
 Pawel Sobocinski
From Swansea:
 Peter Mosses
From Genoa (Italy):
 Giuseppe Rosolini
From Kent: