Lab Lunch Talks Schedule

I will demonstrate an application for displaying Mandelbrot Curves and Julia Curves that responds in real time, implemented by an MSc student, Iain Parris. I'll review some of the theory, demonstrate a phenomenon I've not seen described elsewhere, and pose some questions.

We implement statically-typed multi-holed contexts in OCaml using an underlying algebraic datatype augmented with phantom types. Existing approaches require dynamic checks or more complex type systems. In order to support concatenation we use two type parameters to represent the number of holes in a context as the difference between two Peano numbers. In order to support plugging a context with contexts of different arity we introduce a datatype of lists of contexts of length n with a total of m holes. Further, we extend our representation to allow holes to be marked with additional type information. As an example, we use these marks to implement statically-typed multi-holed XHTML contexts. We take advantage of Garrigue's relaxed value restriction.

When the technology to build quantum computers finally becomes available, it is highly likely that it will only be accessible to a handful of centers around the world. Much like today's rental system of supercomputers, users will probably be granted access to the computers in a limited way. This begs the question: how will the users interface with the quantum computer? We present the first protocol which allows Alice to have Bob carry out a quantum computation for her such that Alice's inputs, outputs and computation remain perfectly private, and where Alice does not require any quantum computational power or memory. She only needs to be able to prepare single qubits from a finite set and send them to Bob, who has the balance of the required quantum computational resources. Our protocol is interactive and from Alice's point of view, can be implemented with physical systems that are already available and well-developed.

I shall give a report on the Workshop on XML, Logic, and Automata held in Grantown-on-Spey in July, just before the ICMS workshop on Logic and Algorithms here. I'll mention some of the memorable talks and give abridged versions of two less memorable talks (given by me: one introduced an analog of the Vardi-Wolper construction for reasoning about XML, and the other introduced the basics of whisky tasting).

A finite automaton over a unary alphabet can be thought of as recognizing a set of numbers. A standard undergraduate result is that this set is always representable as a union of arithmetic progressions. In particular, if we start with a deterministic automaton, then we can compute such a representation in linear time. [We use unary representation for numbers to strengthen the result.] A slightly less well-known result proven by Marek Chrobak in the late 80's is that, if we are given a nondeterministic automaton, then there *exists* an equivalent representation as a union of arithmetic progressions incurring only a quadratic blow-up. However, it is an open problem whether there exists a polynomial time that can compute such an equivalent representation given a nondeterministic automaton as input. Chrobak's original construction runs in exponential time and only very recently it has been improved to quasi-polynomial time. Mere curiosity aside, a polynomial-time algorithm for this problem will yield a substantial improvement in some model checking problem and NFA minimization problem for unary languages. In this talk, I intend to give Chrobak's original construction and, if time permits, Litow's recent improvement to quasi-polynomial time.

Sannella: Journals in Computer Science I am editor-in-chief of the journal Theoretical Computer Science. I will talk about what goes on behind the scenes at a journal and some of the issues in scientific publishing, including the currently fairly hot issue of open access. My journal is published by Elsevier, the world's largest commercial publisher of science journals, and my views are partly coloured by that fact, but in this talk I will not be speaking for Elsevier.

Gilmore: "Partial Evaluation of PEPA Models for Fluid-flow Analysis". We present an application of partial evaluation to performance models expressed in the PEPA stochastic process algebra. We partially evaluate the state-space of a PEPA model in order to remove uses of the cooperation and hiding operators and compile an arbitrary sub-model into a single sequential component. This transformation is applied to PEPA models which are not in the correct form for the application of the fluid-flow analysis for PEPA. The result of the transformation is a PEPA model which is amenable to fluid-flow analysis but which is strongly equivalent to the input PEPA model and so, by an application of Hillston's theorem, performance results computed from one model are valid for the other. We apply the method to a Markovian model of a key distribution centre used to facilitate secure distribution of cryptographic session keys between remote principals communicating over an insecure network. [This is joint work with Allan Clark, Adam Duguid and Mirco Tribastone.]

It is now fairly common to be at a seminar where the speaker expresses surprise that the projected colours are not what he/she saw on the computer display. I will discuss the issues involved with getting consistent colour in the digital domain and explain why it would be surprising if the colours were right (for the systems as used). The talk will be based around the notion of a workflow, e.g., from scanner to display and to printer. I will illustrate briefly the use of some analysis tools which are useful in making compromises forced on us by significant differences in colour gamut of the various stages. This is a recreational talk and no previous knowledge will be assumed. It will last around 50 minutes.