Programme

12:00-13:00
Lunch

Lunch will be served in the downstairs hall.

13:00-14:00
Andy Gordon (Microsoft Research and University of Edinburgh), Tabular: A Schema-Driven Probabilistic Programming Language

Based on joint work with Thore Graepel, Nicolas Rolland, Claudio Russo, Johannes Borgstrom, and John Guiver

We propose a new kind of probabilistic programming language for machine learning. We write programs simply by annotating existing relational schemas with probabilistic model expressions. We describe a detailed design of our language, Tabular, complete with formal semantics and type system. A rich series of examples illustrates the expressiveness of Tabular. We report an implementation, and show evidence of the succinctness of our notation relative to current best practice. Finally, we describe and verify a transformation of Tabular schemas so as to predict missing values in a concrete database. The ability to query for missing values provides a uniform interface to a wide variety of tasks, including classification, clustering, recommendation, and ranking.

For more info, please see (http://research.microsoft.com/fun)[http://research.microsoft.com/fun]

14:00-14:30
Coffee Break

14:30-15:00
Davide Ancona (University of Genoa), Sound and complete subtyping between coinductive types for object-oriented languages

In object-oriented programming, recursive types typically correspond to inductively defined data structures; however, objects can also be cyclic, and inductive types cannot represent them so precisely as happens for coinductive types. We study semantic subtyping between coinductive types with records and unions, which are particularly interesting for object-oriented programming, show cases where it allows more precise type analysis, and develop a sound and complete effective algorithm for deciding it.

15:00-15:30
Joseph Davidson (Heriot-Watt), Models and Modalities

In this talk I will attempt to examine the relationship between the size of a program written in a particular language and the expressiveness of the semantics of that language. We compare across the program/memory boundary using Random Access Stored Program (RASP) machines as a Von Neumann model, and the classic Turing Machine as our Harvard architecture. But will also iterate on our RASP machine to see how minor semantic changes affect our program sizes within a single memory model.

In addition, I explain how semantics are not as suitable as we’d like for these comparisons and use this to motivate how I have grounded our models using Field Programmable Gate Arrays. I’ll will present the current results from both the program+semantics analysis and grounding into FPGAs.

15:30-16:00
Alexander Konovalov (St Andrews), Recomputation in Scientific Experiments

Reproducibility of scientific experiments is crucial for science. However, computational experiments are rarely replicated, and even when the source code has been made available, this may be still far away from running it to replicate the same results.

We claim that it should be as easy to reproduce a computational experiment as to reproduce the chemical reaction from a textbook by mixing baking soda and lemon juice in your kitchen. I will present the project Recomputation.org which suggests how we could make this happen.

16:00-16:30
Coffee Break

16:30-17:00
Adam Barwell (St Andrews), Using Erlang Skeletons to Parallelise Realistic Medium-Scale Parallel Programs

With multi-core processors now standard, the performance boost that came with each single-core generation is no longer free. Parallelism allows a program to take full advantage of the hardware upon which it is run, and so achieve performance gains. Yet despite the dramatic shift in hardware, parallelism techniques have not kept pace. Current techniques are often ad hoc, featuring low-level libraries that require expert knowledge of locks, synchronisation, communication, etc. As the average programmer is not expert in parallelism, parallel programming remains difficult and error-prone. What is needed is a means to help programmers think parallel.

Erlang provides some reprieve, featuring a concurrency model that handles lightweight processes, load balancing, and simple message passing. With a scalable concurrency model, and higher-order functions affording flexible abstraction, Erlang is well suited to embrace parallelism. Yet Erlang’s primitives are still low-level, requiring the programmer to manually manage processes and message passing.

An algorithmic skeleton is an abstract computational entity that models some common pattern of parallelism. Skeletons are typically implemented as high-level functions, abstracting away low-level operations. Skel is an Erlang DSL that provides fundamental and classical skeletons that are easily introduced, replaced, and nested.

In this talk, we present three medium-scale use cases: the Discrete Haar Wavelet Transform, the Single Total Weighted Tardiness Problem using Ant Colony Optimisation, and an image merge. Using Skel, and a 24 core shared memory machine, we parallelise these use cases, demonstrating that with relatively little effort the Skel library can be used to simply parallelise Erlang applications and obtain good speedups.

17:00-17:30
Fredrik Nordvall Forsberg (Strathclyde), Restricted dependent bounded linear types for arbitrary resources

I present a type system for resource allocation, parameterised by an arbitrary notion of resource as in Ghica and Smith’s “Bounded Linear Types” and Brunel, Gaboardi, Mazza, and Zdancewic’s “Coeffect Calculus”. Compared to loc. cit., this system includes a restricted notion of data dependency implemented by indexing type judgements over simple index and resource languages, which is a simplification of Dal Lago and Gaboardi’s “Linear Dependent Types”. The motivation of this work is to provide a fairly precise resource analysis (for arbitrary resources) in the type system while allowing a simple type-inference algorithm. In this talk I justify the design decisions behind the type system and illustrate it with simple examples (and non-examples). The main technical contribution is a coherent categorical semantics using indexed categories. (This is joint work with Dan Ghica.)

17:30-20:00
Pub

After-workshop in Duke’s corner.