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
See all Wessex sites involved and meetings so far.