SPLV24: Scottish Programming Languages and Verification Summer School, 2024
University of Strathclyde, Glasgow, UK — July 29th to August 2nd
This year, the Scottish Programming Languages and Verification Summer School
will be held at the University of Strathclyde campus in the McCance Building, 16 Richmond Street, G1 1XQ.
The event is organized by the Mathematically Structured Programming group in the Department of Computer and Information Sciences.
For announcements and updates concerning SPLV 2024, please subscribe to our SPLS Zulip stream.
Schedule
All talks will take place on level 3 of the McCance Building (follow the signs from the building entrance at 16 Richmond street).
The invited and core courses will take place in room MC301. The specialised courses will take place in rooms MC301 and MC319.
|
Monday |
Tuesday |
Wednesday |
Thursday |
Friday |
08:30 |
|
|
|
|
|
09:00 |
Conor MC301 |
Chris MC301 |
Vikraman MC319 | Andrés MC301 |
Bob MC301 | Sam MC319 |
09:30 |
10:00 |
Conor MC301 |
|
Kathrin MC301 | Jules MC319 |
Vikraman MC319 | Andrés MC301 |
10:30 |
|
Bob MC301 | Sam MC319 |
11:00 |
Chris MC301 |
|
|
|
11:30 |
Jean-Marie MC301 |
Jean-Marie MC301 |
Jean-Marie MC301 |
Jean-Marie MC301 |
12:00 |
12:30 |
|
|
|
|
|
13:00 |
13:30 |
Conor MC301 |
Vikraman MC319 | Andrés MC301 |
Bob MC301 | Sam MC319 |
Kathrin MC301 | Jules MC319 |
14:00 |
14:30 |
Bob MC301 | Sam MC319 |
Kathrin MC301 | Jules MC319 |
|
15:00 |
|
|
15:30 |
Chris MC301 |
|
|
16:00 |
Kathrin MC301 | Jules MC319 |
Vikraman MC319 | Andrés MC301 |
16:30 |
17:00 |
Lightning |
Lightning |
|
17:30 |
|
|
|
18:00 |
18:30 |
19:00 |
|
19:30 |
|
20:00 |
20:30 |
Core Courses
These required lectures cover foundational knowledge.
- Category Theory
- Lecturer: Chris Heunen
Slides: Monday and Tuesday combined
-
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 Mc Bride
Slides: Document camera scans, Agda code
-
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.
- Introduction to Separation Logic
- Invited Lecturer: Jean-Marie Madiot
Slides: Combined
-
Abstract
Separation Logic is a program logic for reasoning on shared mutable data structures
that is also robust enough to be used in the verification of real programming
languages. These lectures are intended to be a gentle but precise introduction
to Hoare logic, weakest preconditions, then separation logic operators and
representation predicates for lists and more higher-order data structures.
We will see how to reason with and without sharing, garbage collection,
higher-order functions, resources, parallelism and concurrency, and effect handlers.
I will also give you a taste of the concurrent separation logic framework Iris,
and will make a few demos.
Unfortunately our original invited course had to be cancelled due to
Covid, and was replaced by the course above.
Cancelled course details
- 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.
Track 1
- Type Theory & Implicit Complexity
- Lecturer: Bob Atkey
Slides: Tuesday, Wednesday, Thursday, Friday
-
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
Slides: Combined
-
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
Slides: Friday (lecture notes to come)
-
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
Slides: Combined
-
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
Slides: Tuesday, Wednesday and Thursday, Friday
-
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
Slides: Tuesday, Thursday AM, Thursday PM
-
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:
- string diagrams as 2-dimensional syntax, how they unify computation graphs and flowcharts
- traced, compact closed and hypergraph categories, non-well-founded recursion, backtracking and quantum processes
- decorated and structured cospans, the standard sledgehammer for building domain-specific categories of open systems
- bidirectional processes: lenses, optics, containers, differentiable programming, categorical cybernetics
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.
Lightning talks
We will have two lightning talk sessions at the end of Monday and Tuesday for students to give a quick introduction to their research. More information including the schedule and talk titles here.
Evening activities and excursion
On Monday evening, after the lightning talks, we will have a social event with free pizza and drinks. This will take place on level 11 of Livingstone Tower, next door to the McCance building, with views over Glasgow.
On Tuesday evening, we will have the summer school dinner in Madha in the Merchant City part of Glasgow. Food and reasonable drink is included in your registration.
On Wednesday afternoon, we will take a local train to Pollok Country Park (train station: Pollokshaws West), which is on the outskirts of Glasgow. There is the opportunity to go for a walk in the park (and watch the highland cattle!), admire the formal gardens of Pollok House, or visit the Burrell Collection (free entry), an award-winning art museum.
Covid mitigation
If you can, please take a Covid test before attending the school, and obviously do not attend if you are not feeling well. Feel free to wear a mask during lectures, if you want – some FFP2 masks will be available for anyone that wants them.
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.
Lectures will take place on the third floor of the McCance Building on the University of Strathclyde campus. There will be signs directing you from the entrance of the building, which is on the north side of the building, on Richmond Street.
There are many hotels in and around the city centre, as well as some hostels.
The very nearest hotels to the university are:
- Premier Inn George Square (100m)
- Moxy Merchant City (250m)
- Z Hotel Glasgow (300m)
- AC Hotel by Mariott Glasgow (300m)
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.
The summer school is generously sponsored by the Scottish Informatics and Computer Science Alliance, Quantinuum, Well-Typed, and Tweag.
Gold
Bronze
Registration
Registration closed Sunday 14 July.
The registration fees are:
- Free
- for students at a SICSA-affiliated university (limited places)
- 250.00 GBP
- for students at non SICSA-affiliated universities and academics
- 750.00 GBP
- for all other participants, i.e. industry practitioners and independent researchers
For students and academics, we kindly request that you register with an institutional account.
If you are unsure which fee is applicable to you, please do get in contact.
Fees cover: all lecture courses, tea and coffee breaks, lunch, a social event on Monday evening, and conference dinner Tuesday evening.
Fees do not cover: travel and accommodation nor subsistence outside of the Summer School times.
A list of options for accommodation are provided below.
If you have any further questions please get in contact with the local organising team at:
The principal organisers of SPLV24 are: