Scottish Programming Languages Seminar

Wednesday 9th March 2022

The Scottish Programming Languages Seminar (SPLS) is an informal meeting for the discussion of any aspect of programming languages. This edition of SPLS will be hybrid, meaning it will be possible to attend this seminar either in-person or online. Physically, the seminar will be held at the Informatics Forum, The University of Edinburgh on Wednesday 9th March 2022. Lunch and coffee will be provided for the in-person attendees.

Information and updates about the March 2022 edition of SPLS will be communicated via the SPLS Mailing List.

This meeting is funded by SICSA and The Royal Society.

Scottish Informatics & Computer Science Alliance The Royal Society


Each talk slot is 25+5 minutes, meaning the speaker has at most 25 minutes for presentation, the remaining 5 minutes are reserved for questions.

Time Speaker(s) Title & Abstract
12:00 Lunch
 Session 1: A differentiated future
  • Conor McBride
  • Sam Lindley
  • Simon Gay
Launching the Scottish Programming Languages Institute

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.

13:30 James McKinna Automatic differentiation, in forward- and reverse-mode, as a one-liner

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).

14:00Coffee break
  Session 2: Data {types,science}
14:30 Xueying Qin Property-based container data types

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.

15:00 Robert Wright Idris Type-Driven Data Science

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.

15:30Coffee break
  Session 3: Stay safe
16:00 Bastian Köpcke Descend: A safe GPU systems programming language

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.

16:30 Jeremy Singer Capability Boehm: Challenges and Opportunities for Garbage Collection with Capability Hardware

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.


It is possible to attend the meeting in one of two ways: in-person or remotely via a video conferencing platform. In either case we ask that you register (see below) such that we can allocate adequate resources to support both attendance modes.

Remote participation

The talks will be live streamed on Zoom as well as on the SPLS YouTube channel. Both streams will go live before 13:00 GMT. The details for the Zoom room are available on the #spls channel on Zulip.

Remote attendees can ask questions to speakers live via Zoom by either using the raise hand feature or typing the question directly into the Zoom room chat or posting it on the topic stream on Zulip.

In-person participation

At the time of writing we are allowed a maximum of 50 in-person attendees. Every in-person attendee must follow the following rules.

The in-person component will take place in room G.07. Lunch and coffee breaks will also take place in G.07. All will be signposted on the day.

Loading interactive map...


If you plan to attend this seminar, then please register in advance using the Doodle form. Registration is especially important for those who wish to attend the in-person component as for safety reasons we only allow those who signed up in advance to participate in-person on the day.


The organisers of this meeting are Daniel Hillerström ( and Frank Emrich (, please contact them directly with any questions regarding this meeting.