School of Computer Science, University of St Andrews, April 26th to 28th 2017

The BCTCS 2017 will take place in Lecture Theatre 3 and Lecture Theatre 4, in the basement of the Gateway Building. Laszlo Babai’s LMS Keynote Lecture will be in Lecture Theatre D of the Mathematical Institute Building.

Wednesday, 26th April 2017

09:30 - 09:50 Registration Opens
09:50 - 10:00 Welcome
10:00 - 11:00 Truthful Outcomes from Non-Truthful Position Auctions (Felix Fischer)
11:00 - 11:30 The complexity of Boolean surjective VCSPs (Peter Fulla)
11:30 - 12:00 Meet & Greet
12:00 - 12:30 Building a better Mouse Maze (Jessica Enright)
12:30 - 13:00 Approximately Enumerating Small Witnesses (Kitty Meeks)
13:00 - 14:00 Lunch
14:00 - 15:00 Bisimulations, Bidirectionality, and the Future of Software Engineering (Perdita Stevens)
15:00 - 15:30 The Relative Proof Complexity of Modal Resolution Systems (Sarah Sigley)
15:30 - 16:00 Canonical Images of Sets in Permutation Groups (Chris Jefferson)
16:00 - 16:45 Refreshments and Discussion
17:00 - 18:30 László Babai LMS Keynote (Mathematical Institute Building, Lecture Theatre D)
19:00 Social Event at St Andrews Brewing Company (map)

Thursday, 27th April 2017

09:30 - 10:30 State Machines All The Way Down (Edwin Brady)
10:30 - 11:00 Adding Erasure to Dependently Typed Programming (Matúš Tejiščák)
11:00 - 11:30 Refreshments and Discussion
11:30 - 12:00 Effects for Lazy Languages (Dylan McDermott)
12:00 - 12:30 Coercive Subtyping in Signatures (Georgina Elena Lungu)
12:30 - 13:00 Reversing Simple Imperative Programs (James Hoey)
13:00 - 14:00 Lunch
14:00 - 15:00 Syntax: What’s it like? (Conor McBride)
15:00 - 15:30 Refreshments and Discussion
15:30 - 17:00 László Babai Seminar
17:00 - 17:30 BCTCS Annual General Meeting
19:00 Dinner at Forgan’s St Andrews (map)

Friday, 28th April 2017

9:30 - 10:30 Monoids, Vectors, and Tensors for Natural Language (Mehrnoosh Sadrzadeh)
10:30 - 11:00 Subwords and Stars (Tom Bourne)
11:00 - 11:30 Refreshments and Discussion
11:30 - 12:00 Modelling Multi-Valued Networks using Rewriting Logic (Obad Abdullah Alhumaidan)
12:00 - 12:30 Formal Semantics for UML State Machines (Tobias Rosenberger)
12:30 - 13:00 Annotated Streaming Protocols for Data Analysis (Chris Hickey)
13:00 - 13:05 Closing Session
13:05 - 14:00 Lunch

LMS Keynote Lecture

This years LMS Keynote Lecture will be given by Professor László Babai (University of Chicago).

Graph Isomorphism I

We discuss the group theoretic aspects at the core of recent progress on the Graph Isomorphism problem: a lemma (the “Unaffected Stabilizers Lemma”) and its algorithmic application (the “Local Certificates algorithm”). The latter produces a canonical structure, breaking the symmetry that has been the bottleneck for Luks’s classic (1980) Divide-and-Conquer strategy.

(Seminar) Graph Isomorphism II

We begin with further details of the group theory involved in the Graph Isomorphism algorithm, followed by a discussion of the combinatorial techniques. Classical (binary) and higher (k-ary) coherent configurations will be the central objects of the discussion.

Professor László Babai will also give a talk at the Scottish Combinatorics Meeting on the 25th of April, and has kindly agreed to give an introductory course for students on the 29th of April, organised by SUMS and STACS.

Invited Talks

Perdita Stevens (University of Edinburgh) - Bisimulations, Bidirectionality and the Future of Software Engineering

A bidirectional transformation is a means of maintaining consistency between two - or more - data sources. In model driven development, the data sources are models: that is, abstract, usually graphical, representations of some aspects of a system. Model driven development has so far been successful in some contexts, but not others; a difficulty that remains is how to make it sufficiently agile, while retaining the advantages it presents where it works. The vision of future software engineering that I plan to put before you involves groups of people who are experts in something but not necessarily software developers, each working with their own model, and using bidirectional transformations to manage consistency between them. I will explain (something about) why that would be a good thing, what needs to happen for the vision to become reality, and what bisimulations have to do with it.

Conor McBride (University of Strathclyde) - Syntax: What’s it like?

When we write programs or prove theorems about a programming language, the first thing we often do is write down a datatype for its syntax. But a syntax is not just any old datatype: there are are usually notions of “scope” and “sort” which impose structure on terms and drive the implementations of operations such as substitution. In this talk, I’ll adapt the technology of datatype-generic programming to the specific needs of types for syntax, showing how types and operations can be generated from a first class notion of grammar. Why keep a dog and bark yourself?

Felix Fischer (University of Glasgow) - Truthful Outcomes from Non-Truthful Position Auctions

The area of mechanism design is concerned with the development of algorithms that produce good outcomes given inputs from self-interested individuals. One of the stars of mechanism design theory is the Vickrey-Clarke-Groves (VCG) mechanism, which makes it optimal for each individual to truthfully reveal its input. In the real world, however, the VCG mechanism is used with surprising rarity and the mechanisms we actually find are non-truthful. An example of this phenomenon are position auctions used by internet search engines like Google and Bing to allocate space for advertisements displayed next to genuine search results. Here only non-truthful mechanisms have ever been used, and what in theory looks like a beginner’s mistake was a huge success in practice. An obvious advantage of the non-truthful mechanisms is that they use simpler payments, and it has been known for some time why this simplicity does not lead to chaos when participants decide strategically how to bid. We will see that the simplicity of payments also comes with a greater robustness to uncertainty on part of the search engines regarding the relative values of positions. The talk is based on joint work with Paul Dütting (LSE) and David C. Parkes (Harvard).

Edwin Brady (University of St Andrews) - State Machines All The Way Down

A useful pattern in dependently typed programming is to define a state transition system, for example the states and operations in a network protocol, as an indexed monad. We index each operation by its input and output states, thus guaranteeing that operations satisfy pre- and post-conditions, by typechecking. However, what if we want to write a program using several systems at once? What if we want to define a high level state transition system, such as a network application protocol, in terms of lower level states, such as network sockets and mutable variables?

In this talk, I will present an architecture for dependently typed applications based on a hierarchy of state transition systems, implemented in a generic data type ST. This is based on a monad indexed by contexts of resources, allowing us to reason about multiple state transition systems in the type of a function. Using ST, we show: how to implement a state transition system as a dependent type, with type level guarantees on its operations; how to account for operations which could fail; how to combine state transition systems into a larger system; and, how to implement larger systems as a hierarchy of state transition systems. I will illustrate the system with a high level network application protocol, implemented in terms of POSIX network sockets.

Mehrnoosh Sadrzadeh (Queen Mary University of London) - Monoids, Vectors, and Tensors for Natural Language

Formalising different aspects of natural language has kept computational linguistics, logicians, and mathematicians busy for decades. On the syntactic side, we have Chomsky and generative grammars from 50’s, Ajdukiewicz and Bar-Hillel and functional grammars from 30’s, Lambek and residuated monoids from 50’s (to name a few). On the semantic side, we have the seminal work of Montague on lambda calculus and higher order logics. Recently, distributional semantics, which is based on Firth and Harris’s insights, has become a successful method of representing meanings of words. This method takes advantage of vectors and linear algebra to reason about the information encoded in large quantities of data, available in the form of text and corpora of documents. I will present the work of my colleagues and I on extending distributional semantics from words to phrases and sentence. In order to realise this passage, we use a notion of grammatical compositionality formalised by Lambek, also employed in other categorial grammars such as the CCG. Our model relies on the notion of tensors and operations from multilinear algebra. I will present the theory behind the model and its applications to natural language tasks such as phrase and sentence similarity, paraphrasing, classification, and entailment. In many occasions the predications of the tensor models better those of simple vector addition and multiplication.

Contributed Talks

Kitty Meeks - Approximately enumerating small witnesses

Although much of the theory of computational complexity focusses on decision problems (“does this problem have at least one solution?”), in many applications we actually need to know how many such solutions there are, or indeed to find all solutions. Of course, the problems of counting and enumerating all solutions are at least as hard as the corresponding decision problem, and in many cases (up to standard complexity theoretic assumptions) these versions of the problem are provably harder than the decision version. The difficulty of counting solutions exactly has led to extensive research into the feasibility of approximate counting, but as yet there is no accepted definition of a corresponding notion of “approximate enumeration”. In this talk I will propose a definition of approximate enumeration, and show how recent work on the enumeration of small witnesses using a deterministic decision oracle (presented at IPEC 2016) can be adapted to enumerate small witnesses approximately when only a randomised decision procedure is available.

Peter Fulla - The complexity of Boolean surjective VCSPs

Boolean valued constraint satisfaction problems (VCSPs) are discrete optimization problems with the goal to find an assignment of labels {0, 1} to variables that minimizes the objective function given as a sum of constant-arity constraints. In the surjective setting, an assignment is in addition required to use each label at least once. For example, the minimum cut problem falls within this framework. We give a complexity classification of Boolean surjective VCSPs parameterized by the set of available constraints.

Tobias Rosenberger - Formal semantics for UML State Machines

UML diagrams are widely used for specifying the desired structure and behaviour of software. However, it is not entirely clear what such a specification means. UML still has no formal semantics and the informal semantics are not precise enough to be formalised in a straightforward way.

One project for solving this problem is based on the theory of institutions, a formalisation of the notion of a logic. The idea is to define an institution for each UML diagram type, thereby increasing modularity and reducing the complexity of each individual logic. Institutions come with a notion of semantics-preserving translations both between different signatures of one logic and between different logics. This allows for heterogeneous reasoning and tool support (theorem provers, model checkers, code generation, etc.).

We present a modal logic we developed for classes of UML state machines which allows us to control the presence or absence of transitions. With this approach we fix a violation of the preservation of semantics under translation between signatures which we discovered in previous attempts at institutionalising UML state machines.

Dylan McDermott - Effects for Lazy Languages

Effect systems augment types with information about the behaviour of programs. They have been used for many purposes, such as optimizing programs, determining resource usage, and finding bugs. So far, however, work on effect systems has largely concentrated on call-by-value languages. We consider the problem of designing an effect system for a lazy language. This is more challenging because it depends on the ability to locate the first use of each variable. Coeffect systems which track contextual requirements of programs, provide a method of doing this. We describe how to track variable usage in a type system for a call-by-need lambda calculus using coeffects. We then add effects to the resulting system, allowing work that has been done on effect systems for call-by-value languages to be applied to lazy languages. We also show that classical strictness analysis appears as a special case of our lazy effect system.

Obad Abdullah Alhumaidan - Modelling Multi-Valued Networks using Rewriting Logic

Qualitative modelling is a technique that is used to integrate the elds of theoretical computer science and the physical and biological sciences. Qualitative modelling aims to model the behaviour of systems without xing the exact quantitative dynamics. Multi-Valued Networks (MVNs) provide a powerful qualitative modelling approach for biological systems, they extend the well-known Boolean Networks by allowing entities state value to be within a range of discrete set of values instead of just 0 and 1. The state of each of each state in an MVN is aected by other entities in the network, and entities can update their values synchronously or asynchronously. While a range of support tools exist for MVNs, such as GINsim, there is still a need for further tool support to be developed to aid the practical application and utilization of MVN techniques. In this presentation we will give an overview of recent work on modelling MVNs using Rewriting Logic! (RL), an algebraic formalism where states are dened using equational specications and the dynamic behaviour of the systems is spec- ied using rewrite rules. Translating MVNs synchronous (where some rewrite strategies are needed) and asynchronous behaviours into rewrite rules and give some illustrative case studies based on using Maude.One of the advantages of RL is the strong tool sup- port and we make use of Maude, a high-performance re ective language supporting both equational and rewriting logic to represent the MVN behaviour. Maud! e is commonly used in metalanguage applications, where it is used to create executable environments for dierent languages and models of computation. We dene a formal translation of asynchronous and synchronous MVNs into RL, and model the MVN behaviour using RL. In particular, the synchronous version required the use of rewriting strategies which demonstrates the exibility of RL. After that, correctness proofs were done for these translations based on showing they are sound and complete. We worked with a range of case studies (e.g. Tryptophan biosynthesis genetic network) to illustrate our translation, and how Maude’s model checking capabilities can be used to analyse an MVN model (using the Maude Search command and Linear Temporal Logic (LTL)). Performance testing was carried out using a scalable test model which again illustrates the exibility of Maude and RL since we could easily dene an extendible model.

Georgina Elena Lungu - Coercive Subtyping in Signatures

It has been shown that adding subtyping to type theories with canonical objects, such as Martin-Lof’s type theory and Luo’s UTT, requires a different understanding than the one employed by programming languages in the form of subsumptive subtyping. I will present a type system with coercive subtyping entries in signatures which can be used to embed a subsumptive subtyping system, giving a way to reason about it in type theories with canonical objects. At the same time the system can itself be embedded in the previously developed coercive subtyping system, hence bridging between the practical notion of subsumptive subtyping and the theoretical coercive subtyping.

Sarah Sigley - The Relative Proof Complexity of Modal Resolution Systems

Proof complexity measures how efficiently theorems can be proved in a given proof system. We compare the strength of two proof systems via polynomial simulations; given two proof systems P and Q we say P polynomially simulates Q if given any Q proof we can efficiently construct a corresponding P proof. Whilst proof complexity has traditionally focused on proof systems for propositional logic, recently work has also been carried out regarding the proof complexity of n! on-classical logics, including modal logics. One motivation for studying the proof complexity of modal logics is that, due to their additional expressiveness compared with propositional logic they are suited to a wide variety of applications throughout computer science. Resolution is a very simple calculus for propositional logic, consisting of only a single inference rule. Over the past 30 years several different resolution calculi have been proposed for modal logics, however no work has been carried out regarding the complexity of these calculi. I will give an overview of two modal resolution calculi, proposed in 1989 and 2007 respectively. I shall then discuss the relative complexity of these calculi, outlining a proof that they both polynomially simulate one another and so are polynomially equivalent, despite being technically rather different. To conclude I will discuss whether certain lower bound proving techinques for propositional resolution might also be applied modal resolution systems.

Jessica Enright - Building a better mouse maze

Mouse Maze is a Flash game about Squeaky, a mouse who has to navigate a subset of the grid graph using a simple deterministic rule, which naturally generalises to a game on arbitrary graphs with some interesting chaotic-looking dynamics. We present efforts to generate graphs which effectively trap Squeaky in the maze for long periods of time, and some theoretical results bounding how long he can be trapped. We show that Squeaky can always escape the graph in finite time, but Squeaky can be trapped forever if he cannot count properly.

Tom Bourne - Subwords and Stars

In the field of formal language theory, the generalised star-height problem asks whether or not there exists an algorithm to determine the minimum nesting depth of stars required in order to represent a given regular language by a regular expression. In this setup, we consider complement as a basic operator. In particular, it is not yet known whether there exist languages of generalised star-height greater than one. We consider the generalised star-height of the languages in which a fixed word occurs as a contiguous subword an exact number of times and of the languages in which a fixed word occurs as a contiguous subword modulo a fixed number, and see that in each case it is at most one.

James Hoey - Reversing Simple Imperative Programs

We propose an approach for reversing simple imperative programs. Inspired by the Reverse C Compiler of Perumalla, we produce both an augmented version and a corresponding inverted version of the original program. Augmentation involves saving necessary information into an auxiliary data store, maintaining segregation between this reversal information and the program state, while never altering the data store in any other way than that of the original program. Inversion uses this information to revert the final program state to the state as it was before execution. At the same time, the final auxiliary store is reversed to its initial state, as the reversal information is removed as it is used. We prove that augmentation and inversion work as intended, and illustrate our approach with several examples. Potential applications include PDES and debugging.

Matúš Tejiščák - Adding Erasure to Dependently Typed Programming

In dependently typed languages, we often express algorithms in ways more amenable to reasoning – we program with views, add indices to type families. However, this means that our programs compute with more data – views, proofs, indices – and thus the programs may end up asymptotically slower (e.g. exponential vs. linear) if these additional structures are too big. Experience with Idris indicates that this problem is important for practical programming with dependent types.

In this talk, I will show a dependently typed calculus that has erasure built into its type system, along with inductive type families and pattern matching. The native erasure support allows us to infer erasure annotations from a program, check consistency of these annotations, and then erase everything marked as runtime-irrelevant before execution, thus recovering the intended run-time behaviour. On the side, we get features like dependent erasure or various forms of erasure polymorphism.

Using erasure allows us to write dependently typed programs using the devices we normally use to obtain correctness guarantees, but without the burden of time and memory complexity pessimisation caused by runtime-irrelevant structures present in the executed program.

Chris Hickey - Annotated Streaming Protocols for Data Analysis

As the popularity of outsourced computations increases, concerns about accuracy and trust between the client and the cloud computing service become ever more relevant. Our work aims to provide faster and more practical methods to verify analysis of large data sets, where the client’s memory costs are independent of the size of the data set. We do this by using annotated data streaming methods, in which the cloud computing service provides a short proof alongside the results which can be used to confirm the correctness of the computation. We supply an optimally efficient protocol for verifying matrix multiplication, and use this to provide protocols for ordinary least squares (OLS) and principal component analysis (PCA).

Chris Jefferson - Canonical Images of Sets in Permutation Groups

Many combinatorial and group theory problems are equivalent to finding, given a group G which acts on a set S and two members X and Y of S, if there is a member of G which maps X to Y. If we make S equal to the set of all graphs, and G the group which permutes the vertices of the graphs, then this is equivalent to the graph isomorphism problem. In this talk I consider a similar problem – considering S to contain sets instead of graphs, but allowing G to be any group. When solving this problem in practice, we often use a ``Canonicalizing Algorithm’’ – this function takes elements of S and maps them to a representative in their orbit under G, so if we can map from X to Y, both X and Y will have the same canonical image. When we have many elements of S to consider, using a canonicalising function can greatly improve performance. I will demonstrate a family of new algorithms for finding canonical images. These algorithms make use of the orbit structure of the group to efficiently reduce the amount of search which must be performed to find a canonical image.