15th Wessex Theory Seminar
The fifteenth meeting of the Wessex Theory Seminar will take place at the University of Birmingham on Thursday 19 July 2012.
Travel & Venue
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
Umberto Rivieccio, University of Birmingham
Logics for partial and inconsistent information
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.
Anupam Das, University of Bath
Finer notions of analyticity for proofs
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.
Julian Rathke, University of Southampton
Local memory via layout randomisation
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.
Steve Vickers, University of Birmingham
Arithmetic universes as generalized spaces
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.
Dusko Pavlovic, Royal Holloway, University of London
Monoidal computer: towards cryptography in pictures
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.
Andrzej Murawski, University of Leicester
Algorithmic games for full ground references
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
- Catrin Campbell-Moore
- Anupam Das
- Jim Laird
- Alvin Šipraga
- 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
- Andrzej Murawski
- Björn Lellmann (Imperial)
- Dusko Pavlovic (Royal Holloway)
- Nobuko Yoshida (Imperial)
- Philippa Cowderoy
- Julian Rathke
- Owen Stephens
- Martin Berger
- Bernhard Reus
See all Wessex sites involved and meetings so far.