University of Strathclyde logo

SPLV24: Scottish Programming Languages and Verification Summer School, 2024

Glasgow, UK — July 29th to August 2nd

This year, the Scottish Programming Languages and Verification Summer School will be held in Strathclyde. The event is organized by the Computer and Information Sciences department at the University of Strathclyde.

For announcements and updates concerning SPLV 2024, please subscribe to our SPLS Zulip stream.

Core Courses

These required lectures cover foundational knowledge.

Category Theory
Lecturer: Chris Heunen
Abstract Category theory is a powerful way to describe objects only in terms of how they interact — without looking inside an object to see how it is made. In other words, it focuses on behaviour rather than implementation details. This tool is therefore very useful to think about programming languages and semantics, and relates to type theory. These lectures will start from the beginning, introducing categories and examples. We'll discuss universal properties, which characterise for example products and function types. Next we focus on monads, which are a popular way to capture computational effects, and adjunctions, which provide translations between different categories. Finally, we briefly touch on monoidal categories, string diagrams, and strong monads.
Type Theory
Lecturer: Conor McBride
Abstract What makes type theories tick? I intend these lectures to communicate an approach to the metatheory of type theories which keeps a tight grip on the direction of information flow and of trust. A typing rule is a server for its conclusion and a client for its premises. The places in judgement forms are classified not only grammatically but as signals. Every signal has both a sender (who transmits the syntax of the signal) and a guarantor (who promises that the signal is in some way meaningful). We gain insight by distinguishing inputs (client-sent) from outputs (server-sent), citizens (guaranteed by their senders) from subjects (to be guaranteed by their receivers), and expressions (synthesizing signals to send) from patterns (analysing signals upon receipt). In my first lecture, I shall introduce the approach via a straightforward example: a reformulation of Martin-Löf's 1971 type theory, separating type checking for introduction forms from type synthesis for elimination forms. In my second lecture, I shall explore the metametatheory of the approach, showing generic benefits of its adoption, with some standard metatheoretic properties shifting becoming less things to prove and more things to not mess up. If I'm not massively overrunning by Tuesday morning, I'll have a quick look at how I go about formalising this approach in Agda. You won't find any of this in a book.

Invited Course

Our guest lecture series opens a window to a related field.

A few ideas from distributed systems for PL folk
Invited Lecturer: Lindsey Kuper
Abstract Fifteen years ago, when I was a new PhD student and suffering from an advanced case of PL myopia, I foolishly ignored every other area of computer science. It was only years later that I realized that distributed systems had a lot to teach me. In these lectures, I'll fill you in on what I've learned so far, so you won't be as foolish as I was. We'll start with the very basics (what is a distributed system?) and work our way up to an implementation of causal broadcast, then finish the week with a brief excursion into choreographic programming. No background in distributed systems is necessary, only an open mind.
Bio Lindsey Kuper is an Assistant Professor at the University of California, Santa Cruz. She works on programming-language-based approaches to building concurrent and distributed software systems that are elegant, correct, and efficient. Some of her research contributions include library-level choreographic programming, verification of distributed protocols using refinement types, and guaranteed-deterministic parallel programming with LVars. She co-founded !!Con (bangbangcon.com), the radically inclusive conference of ten-minute talks on the joy, excitement, and surprise of computing. She is the recipient of an ICFP Distinguished Paper Award (2023), an NSF CAREER Award (2022), and a Google Faculty Research Award (2019), and received her Ph.D. in computer science in 2015 from Indiana University.

Specialised Courses

The specialised courses are offered as two tracks running in parallel. The interleaving is currently TBC.

Track 1

Type Theory & Implicit Complexity
Lecturer: Bob Atkey
Abstract Implicit Computational Complexity is concerned with the characterisation of computational complexity classes as programming languages. A programming language characterises a complexity class if every function in that class can be implemented in the language and every function implementable in the language is in the class. In this course I will show how to use Linear Type Theory to characterise the class of Polynomial Time computable functions, and how by using Linear Dependent Types, we can use this describe other classes such as NP, coNP and beyond.
Mechanization of Binders
Lecturer: Kathrin Stark
Abstract Binders are ubiquitous when mechanising results about programming languages. More than 15 years after the POPLMark Challenge, new tools and approaches to binding are still being published, and binders are still frequently mentioned as being the main difference between mechanisation and paper proof. So which one to choose: named, de Bruijn, locally nameless, nominal syntax or HOAS? While not answering this question, this course takes a (necessarily incomplete) peek into several approaches to binders in a programming language, with a focus on their mechanisation.
Category Theory for Semantics
Lecturer: Vikraman Choudhury
Abstract A programming language is a very exotic object: it provides a vocabulary to give instructions to a computer, and at the same time, denotes a mathematical object that follows axioms. The purpose of semantics is to reconcile the two notions, giving insights into computation, language design, and programming. In this course, I will introduce some tools and techniques from category theory that are useful to semanticists, and show applications of these to prove fundamental results about type theories and programming languages.

Track 2

Protocol Verification
Lecturer: Andrés Goens
Abstract Protocols are central to the functioning of many crucial systems. From the consistency of your device's memory, to exchanging information over the internet, protocols ensure these extremely concurrent systems function correctly. In this course we will consider some basic principles required to verify such protocols. We will learn about labeled transition systems and use temporal logic to specify properties of them. In particular, we will focus on safetey and fairness conditions in protocols.
Effects and Handlers
Lecturer: Sam Lindley
Abstract Effect handlers allow programmers to define, customise, and compose a range of crucial programming features ranging from exceptions to lightweight threads to probability, inside the programming language. In this course I will give a high-level introduction to the theory of algebraic effects and effect handlers, effect type systems for effect handlers, and effect handler oriented programming.
Applied Category Theory
Lecturer: Jules Hedges
Abstract This course will be about symmetric monoidal categories and what they have to tell us about computation and systems. I plan the topics of my 4 lectures to be:
  1. string diagrams as 2-dimensional syntax, how they unify computation graphs and flowcharts
  2. traced, compact closed and hypergraph categories, non-well-founded recursion, backtracking and quantum processes
  3. decorated and structured cospans, the standard sledgehammer for building domain-specific categories of open systems
  4. bidirectional processes: lenses, optics, containers, differentiable programming, categorical cybernetics

Details

SPLV 2024 is scheduled to run one full week:

from 9am on Monday 29th July to 2:30pm on Friday August 2nd.

Lectures will run face-to-face on-site. We will use the SPLS Zulip for online communications (e.g. for questions, arrival/dinner on Sunday, …).

Prerequisites:

The school is aimed at PhD students in programming languages, verification and related areas. Researchers and practitioners are very welcome, as are strong undergraduate and masters students with the support of a supervisor. Participants will need to have a background in computer science, mathematics or a related discipline, and have basic familiarity with (functional) programming and logic.

Registration:

TBD

Schedule:

Monday Tuesday Wednesday Thursday Friday
08:30 Registration
09:00
09:30
10:00
10:30
11:00
11:30
12:00
12:30
13:00
13:30
14:00
14:30
15:00
15:30
16:00
16:30
17:00

Sponsorship

Industrial sponsorship is always welcome, and if your company would like to sponsor SPLV 2024 then please do get in contact with the organising team.

Travel and Accommodation

The University of Strathclyde is located a short (five minutes) walk from Glasgow Queen Street, heading east from the City Centre. Glasgow Central Station is 15 minutes away. The University provides travel information including maps and directions. The summer school will be taking place in the McCance Building.

There are many hotels in and around the city centre, as well as some hostels.

The very nearest hotels to the university are:

The Premier Inns at St Enoch Square and particularly Glasgow City Centre South (just south of the River Clyde), are a bit further away (~25 min walk for the latter), but are normally cheaper than their George Square counterpart.

For those willing to share a dorm, the Revolver Hotel (private rooms also available) may be worth a look.

Unfortunately, Strathclyde’s halls of residence are not available this summer due to renovation work. However for those who would prefer a cheap self-catering option, we understand that our city-centre neighbour, Glasgow Caledonian University, currently has availability (~15 minute walk). You would have to email their accommodation office for more information.

Further Information:

If you have any further questions please get in contact with the local organising team at:

The principal organisers of SPLV24 are:

This site is open source. Improve this page.