The fourteenth meeting of the Wessex Theory Seminar was held at the University of Bath on Wed= nesday 23rd May 2012.

=20University of Bath travel information: http://www.bat= h.ac.uk/about/gettinghere/ .

=20All lectures will take place in room 2.1 in the 3 East building (3E 2.1)= . Maps can be found here: http://www.bath.ac.uk/maps/ .

=20From the train station you will have to get a bus or a taxi to campus. I= f you take the bus then ride it to the last stop on campus, the bus stand, = and if you take a taxi do the same. There will (hopefully) be signs from th= ere guiding you to the seminar.

=20**10:30 Coffee**

**11:00 Olle Fredriksson, Birmingham. (** **Website** **,** **Abstract** **,** **Slides** **)**

**11:45 Georg Struth, Sheffield. (** **Website** **,** **Abstract** **)**=20

**12:30 Lunch**

**13:45 Alessio Guglielmi, Bath. (** **Websi=
te** **,** **Abstract** **,** **Slides** **)**

**14:30 James Davenport, Bath. (** **Websi=
te** **,** **Abstract** **,** **Slides** **)**

**15:15 Edmund Robinson, Queen Mary. (** **Website** **,** **Abstract** **)**

**16:00 Coffee**

**16:30 Jim Laird, Bath. (** **Website=
** **,** **Abstract** **)**

**17:15 Uday Reddy, Birmingham. (** **Websit=
e** **,** **Abstract** **,** **Paper** **)**

**18:00 Pub/Dinner**

=20

**Programming semantics in the presence of complex numbers, logari=
thms etc.**

In considering the reliability of numerical programs, it is normal to "l= imit our study to the semantics dealing with numerical precision". On the o= ther hand, there is a great deal of work on the reliability of programs tha= t essentially ignores the numerics. The thesis of this paper is that there = is a class of problems that fall between these two, which could be describe= d as "does the low-level arithmetic implement the high-level mathematics". = Many of these problems arise because mathematics, particularly the mathemat= ics of the complex numbers, is more difficult than expected: for example th= e complex function log is not continuous, and many algebraic simplification= rules are not universally valid.

=20=20

**Towards seamless distributed computing**

We present a seamless approach to writing and compiling distributed code= . By "seamless" we mean that the syntax and semantics of the distributed pr= ogram remain the same as if it was executed on one node only, except for la= bel annotations indicating on what node sub-terms of the program are to be = executed. There are no restrictions on how node labels are to be assigned t= o subterms. We show how the paradigmatic (higher-order functional recursive= ) programming language PCF , extended with node annotations, can be used fo= r this purpose. The compilation technique is directly inspired by game sema= ntics and the Geometry of Interaction.

=20=20

**Towards More Efficient and Natural Proof Systems**

I will illustrate an ongoing research programme aimed at improving the r= epresentation of formal proofs.

=20In recent years we discovered that cut elimination can be performed in a= way that is largely independent of syntax, provided that we are able to co= mpose proofs in more liberal ways than the classical proof theory of Gentze= n permits. That same liberal composition mechanism, that we call deep infer= ence, provides for analytic proofs that are smaller, and so more efficient,= than what Gentzen theory gives us.

=20Now we intend to use deep inference and certain geometric intuitions to = design a new logical formalism where proofs will be represented with a mini= mum of syntax. This way, proof representation will be less idiosyncratic an= d so more natural.

=20=20

**Regular Language Game Semantics for Polymorphism with Dynamic Bi=
nding**

I will present a fully abstract model for a block-structured language wi= th (finite) integer state, higher-rank polymorphism (universal and existent= ial types) and dynamically bound variables. Typing of functions is based on= Reynolds' Syntactic Control of Interference (SCI), which constrains sharin= g of identifiers between procedures. I shall discuss two variants of the ty= ping rule for dynamic binding, corresponding to "strong" and "weak" forms o= f interference control, and focus on the latter as it leads to a simpler, s= trongly sequential model, and can express (bounded) nesting of functions.=20

The categorical structures used to in the semantics are an instance of a= more general notion of model for stateful languages based on dual input an= d output types and an associated trace operator: I shall also discuss conne= ctions with Reddy/McCusker's relational model of SCI. In our semantics, typ= es denote finite fragments of a "universal event structure" , with a questi= on/answer relation used to represent generic "copycat" behaviour. Programs = of a given type denote regular languages over the corresponding set of even= ts. The main result is that the model is sound and complete for program equ= ivalence, which is therefore decidable.

=20=20

**Axiomatizing relational parametricity**

Relational parametricity is a semantic reasoning principle proposed by J= ohn Reynolds, to capture the ideas of data abstraction and information hidi= ng in programs. It is closely related to logical relations, widely used for= proving properties of typed lambda calculi, and simulation and bisimulatio= n relations used for proving the equivalence of data types and processes. I= t is also tantalizingly close to the idea of natural transformations that f= orm the foundation for category, but generalizes them to higher-order types= .

=20In this talk, I present a categorical axiomatisation of the concept, mar= rying the ideas of of reflexive graphs and fibrations. The axiomatisation h= as a wide ranging application for categories other than Set, including alge= braic and other mathematical structures, domains, presheaves, as well as ev= ent-based models. Applications of the axiomatic treatment for the semantics= of polymorphic lambda calculus and the semantics of Algol-like languages w= ill be highlighted.

=20Despite all this progress, much work still remains to be done in various= directions, in exploring connections with various branches of mathematics,= computer science and physics. I hope to indicate what these directions mig= ht be.

=20=20

**Ultrametric spaces, trees and lazy datastructures**

Ultrametric spaces are used as a modelling technology, but in fact are m= ore closely connected to tree-like structures than conventional metric spac= es. The aim of this talk is to explain that relationship and the consequent= link with lazy datatypes.

=20=20

**Semigroups for Concurrency**

Concurrent Kleene algebras have recently been proposed for studying vari=
ous approaches to concurrency in a simple, abstract and uniform way. It tur=
ns out that semigroups, which account for the

interaction between seque=
ntial and concurrent composition, play a crucial role in this investigation=
.

This overviews concurrent Kleene algebras and discusses some of their=
most important models, including shuffle languages and series-parallel pom=
sets. It then explains their relationship to concurrent separation logic an=
d elaborates on the role and potential of semigroup theory for concurrency.=
Since the approach is quite novel, there are so far more questions than an=
swers, some of which will be raised at the end of the presentation.

**Altran Praxis**

Florian Schanda

**Bath**

Ana C. Calderon

Anupam Das

Alessio Gug=
lielmi

Jim Laird

Guy McCusker

John Power

Cai Wingfield

=
David Wilson

James Davenport

Matthew England

Ali El Kaafarani** Mesar Hameed**

**Birmingham**

Olle Fredriksson

Paul Levy

Uday =
Reddy

Chuangjie Xu

Liang-Ting Chen

**Coastline Computer Consultancy**

John Hanson

**Imperial College London**

Faris Abou-Saleh

**Queen Mary**

Edmund Robinson

Paulo Oliva

**Royal Holloway**

Dusko Pavlovic

**Sheffield**

Georg Struth

**Southampton**

Owen Stephens

**Swansea**

Martin Churchill

Peter Mosses

Caspe=
r Bach Poulsen

Ferdinand Vesely

See all Wessex sites i= nvolved and meetings so far.