• Conor McBride
• Sam Lindley
• Simon Gay

We propose to set up a Scottish Programming Languages Institute (SPLI) as an umbrella for activities such as the Scottish Programming Languages Seminar (SPLS), the Scottish Summer School on Programming Languages and Verification (SPLV), various seminar series that have grown beyond their host institutions, and industrial engagement. By formally consolidating the breadth, depth and expertise of programming language research in Scotland, SPLI will provide a platform for future initiatives.

This talk aims to demystify the basics of automatic differentiation (AD) by considering it as an abstract evaluator of symbolic expressions (the 'one-liner' of the title). We further show how to incorporate the mysteries of forward- and backward-mode AD by changing the result type of the evaluation in interesting, but algebraically comprehensible, ways, which moreover realise the successive improvements, in computational complexity, from purely functional vanilla forward-mode AD to imperative, array-based, reverse-mode AD.

Joint work with Birthe van den Bergh, Tom Schrijvers (KU Leuven) and Alexander Vandenbroucke (Standard Chartered).

Container data types such as sets, lists, and trees, represent collections of data that, are commonly used in computer programs. Much work have been done in the past decades to design better abstraction, improve performance and verify correctness for container data types. However, one crucial problem still exists. Currently, when choosing a container data type, programmers can not choose an abstract container only based on the desired container’s behaviours, but they must choose a concrete implementation of that abstract container as well. For example, instead of being able to request a container with unique elements, programmers must choose between possible implementation such as trees or hash sets. One serious drawback is that the chosen concrete implementation cannot provide the desirable performance or memory efficiency in all usage scenarios. Also, the portability of programs is limited as one concrete implementation might only have optimised performance for certain hardware systems.

Traditionally, most data science is done in dynamically typed languages. If you're manipulating a table of data, and make a typo in a column name, or ask for the wrong column, then you don't find out until runtime - after which significant computation may have taken place. So a small mistake could lose a large amount of time.

With dependant types, we can express the schemas of tables at compile-time. This allows us to check, at compile-time, that our columns exist, and are of the correct types.

We will go through a simple machine learning example, and show the whole workflow, to demonstrate how dependant types can help the process.

Programming Graphics Processing Units (GPUs) is a challenging task even for expert programmers. Thousands of GPU threads have to be coordinated to safely make efficient use of the hardware resources. The most common GPU programming language CUDA, a variant of C, offers programmers great control over which thread operates at which time on which memory location. This is essential for achieving high performance but comes with the same memory and concurrency safety challenges well-known in C. High-level languages such as Futhark or RISE address this by severely restricting the programmers' ability to control low-level details and providing fixed common higher level computational patterns, such as map and reduce.

We present a new GPU programming language, Descend, that aims to combine the advantages of both approaches: enabling precise control safely. Descend is heavily inspired by Rust, but addresses additional challenges arising from the GPU hardware. Descend 1) guarantees memory safety in the presence of thousands of parallel executing threads, 2) ensures the correct interaction between CPU and GPU, 3) enforces the GPU’s thread and memory hierarchy.

In this talk, I will present our current status of designing and implementing Descend, which includes a Rust-style affine type system with extended borrowing rules, and a prototype implementation of a compiler generating CUDA code. I will present Descend using examples to highlight how it enforces memory safety while allowing users to maintain control.

The Boehm-Demers-Weiser Garbage Collector (BDWGC) is a production-quality memory management framework for C/C++ applications. In this talk, we explore adapting BDWGC for modern capability hardware, in particular the CHERI system, which provides guarantees about memory safety due to runtime enforcement of fine-grained pointer bounds and permissions. We describe various challenges presented by the CHERI micro-architectural constraints, along with some significant opportunities for runtime optimization.