The fifteenth meeting of the Wessex Theory Seminar will take place at the University of Birmingham on Thursday 19 July 2012.

There is a train station called **University** located next to the campus. Your best option is probably to take a train to Birmingham New Street and then another to University, but there are also direct trains from Cheltenham, Cardiff and Nottingham.

The talks will be held in room B01 in Mechanical Engineering, which is building

Yellow 3 on the campus map, five minutes' walk from the station.

11:15 coffee (room B22)

11:45 **Umberto Rivieccio** Logics for partial and inconsistent information

12:30 **Anupam Das** Finer notions of analyticity for proofs

13:15 lunch - not provided, but we suggest Staff House

14:15 **Julian Rathke** Local memory via layout randomisation

15:00 **Steve Vickers** Arithmetic universes as generalized spaces

15:45 coffee (room B22)

16:15 **Dusko Pavlovic** Monoidal computer: towards cryptography in pictures

17:00 **Andrzej Murawski** Algorithmic games for full ground references

17:45 pub/dinner near to Birmingham New Street

In 1976, Nuel Belnap suggested that a computer should think using a four-valued logic whose space of truth values extends the classical one with two extra values representing, respectively, lack of information and contradictory information. This approach, which generalizes Kleene's three-valued logic, was further generalized in 1988 by Matthew Ginsberg with the introduction of algebraic structures called "bilattices". These structures gave rise to an interesting mathematical theory and have since then been applied in several areas of computer science (e.g., logic programming, non-monotonic reasoning, truth maintenance systems). I will present an overview on bilattices, with particular emphasis on the algebraic and logical aspects on which I have focused my recent research.

In proof theory we traditionally distinguish between proofs with cut and those without, and ones with cut can be made cut-free via normalisation procedures, albeit at an exponential cost in proof size. In the setting of deep inference there are also certain interim forms which balance properties from both classes of proofs. We thus break down traditional normalisation procedures into smaller steps and identify which stages obtain certain properties, as well as analysing their complexity. In particular we consider an interim class of proofs that seems to enjoy low proof complexity yet also presents advantages for proof search.

Randomisation is used in computer security as a tool to introduce unpredictability into the software infrastructure. In this talk, I'll discuss the use of randomization to achieve secrecy and integrity guarantees for local memory.

Following the approach set out by Abadi and Plotkin (CSF 2010) I'll consider two related idealised languages: in the first, attackers simply cannot access local addresses of the user program. In the second, attackers may attempt to guess allocated memory locations and thus, with small probability, gain access to the local memory of the user program.

Our contribution to the Abadi and Plotkin program is to enrich the idealised languages with dynamic memory allocation, first class and higher order references and call/cc-style control. On the one hand, these enhancements allow us to directly model a larger class of system hardening principles. On the other hand, the class of opponents is also enhanced since our enriched language permits natural and direct encoding of attacks that alter the control flow of programs.

Our main technical result is, in the presence of randomised layouts, a proof that contextual equivalence is preserved (up to a small probability) when moving from one language to the other. Thus the attacker gains no real power from being able to guess local references of the user program.

Joint work with Maria Emilia Maietti, Università di Padova

Joyal's arithmetic universes (AUs) are formalized as pretoposes with

parametrized list objects. This is enough to allow them to interpret not only coherent logic

but also some countable disjunctions, giving a significant fragment of geometric logic -

even though the essentially algebraic theory of AUs is finitary. The work reported here

starts to explore to what extent arithmetic universes can replace Grothendieck toposes in

classifying geometric theories.

A big obstruction is the fact that AUs are not cartesian closed in general. Nonetheless we

have shown an induction principle for proving sequents of the form:

for all k:Nat (P(k)->Q(k)), with an application to locatedness of Dedekind sections.

Along the way we prove various results analogous to what is known for toposes. Two

representation theorems show that adjoining a global element to an object is equivalent to

slicing the AU, and that forcing a subobject of 1 to be 0 (to describe a closed subspace) is

equivalent to going to a simple case of a category of sheaves. We also show that there is a

Boolean algebra of subspaces generated by the opens and the closeds.

Cryptography and complexity theory often involve low level programming of abstract computers, usually Turing machines. Are there better ways to omit the irrelevant implementation details than by describing the constructions semi-formally? The idea of this work is to provide a convenient diagrammatic formalism for reasoning about computability, complexity and randomized computation, based on monoidal categories. The basic computability results, such as Kleene's Fixed Point Theorem, or Rice's Theorem, yield to succinct diagrammatic proofs. Randomized computation is captured using polynomial categories. If the time permits, I will provide a diagrammatic presentation of a typical cryptographic argument.

Joint work with Nikos Tzevelekos, Queen Mary, University of London

We present a full classification of decidable and undecidable cases

for contextual equivalence in a finitary ML-like language equipped

with full ground storage (both integers and reference names can be

stored). The simplest undecidable type is unit -> unit -> unit. At the

technical level, our results marry game semantics with

automata-theoretic techniques developed to handle infinite

alphabets. On the automata-theoretic front, we show decidability of

the emptiness problem for register pushdown automata extended with

fresh-symbol generation.

From Bath:

- Catrin Campbell-Moore
- Anupam Das
- Jim Laird
- Alvin Šipraga

From Birmingham:

- Félix Baschenis
- Ian Batten
- Sergiu Bursuc
- Liang-Ting Chen
- Martín Escardó
- Bertfried Fauser
- Olle Fredriksson
- Dan Ghica
- Achim Jung
- Paul Blain Levy
- Uday Reddy
- Asiri Rathnayake
- Umberto Rivieccio
- Maxim Strygin
- Hayo Thielecke
- Steve Vickers
- Chuangjie Xu

From Leicester:

- Andrzej Murawski

From London:

- Björn Lellmann (Imperial)
- Dusko Pavlovic (Royal Holloway)
- Nobuko Yoshida (Imperial)

From Nottingham:

- Philippa Cowderoy

From Southampton:

- Julian Rathke
- Owen Stephens

From Sussex:

- Martin Berger
- Bernhard Reus

See all Wessex sites involved and meetings so far.