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

University of Bath travel information: http://www.bath.ac.uk/about/gettinghere/ .

All 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/ .

From the train station you will have to get a bus or a taxi to campus. If 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 there guiding you to the seminar.

**10:30 Coffee**

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

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

**12:30 Lunch**

**13:45 Alessio Guglielmi, Bath. (** **Website** **,** **Abstract** **,** **Slides** **)**

**14:30 James Davenport, Bath. (** **Website** **,** **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. (** **Website** **,** **Abstract** **,** **Paper** **)**

**18:00 Pub/Dinner**

**Programming semantics in the presence of complex numbers, logarithms etc.**

In considering the reliability of numerical programs, it is normal to "limit our study to the semantics dealing with numerical precision". On the other hand, there is a great deal of work on the reliability of programs that 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 described as "does the low-level arithmetic implement the high-level mathematics". Many of these problems arise because mathematics, particularly the mathematics of the complex numbers, is more difficult than expected: for example the complex function log is not continuous, and many algebraic simplification rules are not universally valid.

**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 program remain the same as if it was executed on one node only, except for label 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 to subterms. We show how the paradigmatic (higher-order functional recursive) programming language PCF , extended with node annotations, can be used for this purpose. The compilation technique is directly inspired by game semantics and the Geometry of Interaction.

**Towards More Efficient and Natural Proof Systems**

I will illustrate an ongoing research programme aimed at improving the representation of formal proofs.

In 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 compose proofs in more liberal ways than the classical proof theory of Gentzen permits. That same liberal composition mechanism, that we call deep inference, provides for analytic proofs that are smaller, and so more efficient, than what Gentzen theory gives us.

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

**Regular Language Game Semantics for Polymorphism with Dynamic Binding**

I will present a fully abstract model for a block-structured language with (finite) integer state, higher-rank polymorphism (universal and existential types) and dynamically bound variables. Typing of functions is based on Reynolds' Syntactic Control of Interference (SCI), which constrains sharing of identifiers between procedures. I shall discuss two variants of the typing rule for dynamic binding, corresponding to "strong" and "weak" forms of interference control, and focus on the latter as it leads to a simpler, strongly sequential model, and can express (bounded) nesting of functions.

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 and output types and an associated trace operator: I shall also discuss connections with Reddy/McCusker's relational model of SCI. In our semantics, types denote finite fragments of a "universal event structure" , with a question/answer relation used to represent generic "copycat" behaviour. Programs of a given type denote regular languages over the corresponding set of events. The main result is that the model is sound and complete for program equivalence, which is therefore decidable.

**Axiomatizing relational parametricity**

Relational parametricity is a semantic reasoning principle proposed by John Reynolds, to capture the ideas of data abstraction and information hiding in programs. It is closely related to logical relations, widely used for proving properties of typed lambda calculi, and simulation and bisimulation relations used for proving the equivalence of data types and processes. It is also tantalizingly close to the idea of natural transformations that form the foundation for category, but generalizes them to higher-order types.

In this talk, I present a categorical axiomatisation of the concept, marrying the ideas of of reflexive graphs and fibrations. The axiomatisation has a wide ranging application for categories other than Set, including algebraic and other mathematical structures, domains, presheaves, as well as event-based models. Applications of the axiomatic treatment for the semantics of polymorphic lambda calculus and the semantics of Algol-like languages will be highlighted.

Despite 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 might be.

**Ultrametric spaces, trees and lazy datastructures**

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

**Semigroups for Concurrency**

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

interaction between sequential 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 pomsets. It then explains their relationship to concurrent separation logic and elaborates on the role and potential of semigroup theory for concurrency. Since the approach is quite novel, there are so far more questions than answers, some of which will be raised at the end of the presentation.

**Altran Praxis**

Florian Schanda

**Bath**

Ana C. Calderon

Anupam Das

Alessio Guglielmi

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

Casper Bach Poulsen

Ferdinand Vesely

See all Wessex sites involved and meetings so far.