Abstracts

Contributed talks

Invited talks

David S. Johnson

Bin Packing: From Theory to Experiment and Back Again

In the bin packing problem, one is given a list of 1-dimensional items and asked to pack them into a minimum number of unit-capacity bins. This was one of the first NP-hard problems to be studied from the "approximation algorithm" point of view, and over the years it has served as a laboratory for the study of new questions about approximation algorithms and the development of new techniques for their analysis. In this talk I present a brief survey of this history, highlighting the many surprising average case behavior results that have been obtained. Several of these surprises were first revealed by experimentation, which led to conjectures and then to proofs, and I will describe this interplay between experimentation and theory. I'll also highlight some as-yet-unproven conjectures suggested by the experimental data.

Cliff Jones

AI4FM - how to say "why" in proofs

The AI4FM project is exploring how to use AI thinking in discharging proof obligations (POs) that arise in the formal development of programs. Of course, developing better and better heuristics for theorem provers has been explored by AI researchers since its early days. The approach being taken in this project (with Alan Bundy providing the main AI input) is to design a system that can learn from how an expert tackles POs that are beyond current heuristics. We have industrial data that suggests as few as 5 ideas might kill off a hundred undischarged POs. The first step is to design ways of recording the insights which are often about "why" the expert chose a strategy; we will move on to learning such strategies in the next phase of the AI4FM project.

Carsten Witt

Bio-Inspired Computation Meets Theoretical Computer Science

Biologically inspired methods of computation such as evolutionary algorithms, ant colony optimisation, particle swarm optimisation etc. are well established in numerous engineering disciplines. As their computational complexity was generally unknown, these approaches lived in the shadows of theoretical computer science for a long time. This dramatically changed in recent years, when bio-inspired computation was finally perceived as a family of algorithms and analysed using methods from classical algorithms and complexity theory.

This talk will present some of the most exciting results that have been obtained in this new research area. We focus on evolutionary algorithms and ant colony optimisation in combinatorial optimisation and prove how they efficiently find optimal or approximate solutions to problems known from the theory of algorithms.

Prakash Panangaden

Epistemic Strategies and Games on Concurrent Processes

We develop a game semantics for process algebra with two interacting agents. The purpose of our semantics is to make manifest the role of knowledge and information flow in the interactions between agents and to control the information available to interacting agents. We define games and strategies on process algebras, so that two agents interacting according to their strategies determine the execution of the process, replacing the traditional scheduler. We show that different restrictions on strategies represent different amounts of information being available to a scheduler. We also show that a certain class of strategies corresponds to the syntactic schedulers of Chatzikokolakis and Palamidessi, which were developed to overcome problems with traditional schedulers modelling interaction. The restrictions on these strategies have an explicit epistemic flavour. This is joint work with Konstantinos Chatzikokolakis and Sophia Knight, both at INRIA Saclay.

Peter Selinger

Logical methods in quantum information theory

I will talk about some recent applications of logical methods to quantum information theory. In computing, a higher-order function is a function for which the input or output is another function. I will argue that many of the interesting phenomena of quantum information theory involve higher-order functions, although that is not how they are usually presented. I'll talk about the quantum lambda calculus as a possible framework to describe such phenomena.

Nigel Smart

Homomorphic Encryption

The big story in cryptography in the last two years has been the discovery of a Fully Homomorphic Encryption scheme. Such schemes, if made practical, could provide a fundamental paradigm shift in how we build secure online services; such as envisaged by the shift to cloud computing. However, even now we can practically perform interesting advanced applications using standard Homomorphic Encryption. In this talk I will look at some standard Homomorphic Encryption schemes; and describe a voting application. Then I will describe in simple terms how the new Fully Homomorphic Encryption schemes work.