SPLV’26: Scottish Programming Languages and Verification Summer School 2026

The University of Glasgow — 3rd Aug to 7th Aug

The 2026 edition of SPLV will be held at the University of Glasgow, with the main courses running from within our stunning old campus building, the Gilbert Scott Building.

Venue

The main courses will be held in One A, The Square, right next to the University Chapel. A detailed campus map is available here.

Where to go on the day

For registration on Monday, please head to One A, The Square. There you will find members of the organisation committee and we will get you signed-up.

Registration and Accommodation

Registration is now open via Eventbrite.

Registration is priced as:

Academic (early, registration deadline 30th June 2026): £260
Academic (late): £360
Standard (early, registration deadline 30th June 2026): £760
Standard (late): £860

This includes access to all sessions, catered lunch, social events, and a catered reception at Glasgow City Chambers.

We also have a limited amount of subsidised accommodation remaining at £195 for an en-suite room in Queen Margaret Residences, checking in on Sunday 2nd August and checking out on Friday 7th August. You can book this from the registration page.

Course Line-up

This year we have 3 invited core courses, and 6 contributed courses.

Core Courses

Introduction to Types and Lambdas by Nachi Valliappan (University of Edinburgh)

Types were introduced to me as a restriction bolted on top of the untyped lambda calculus to prevent certain runtime errors. Shackles I must program with, because I cannot be trusted with the power of the unruly lambda calculus. In this course, I will present types through the lens of a different paradigm, where types are internalized into the definition of the calculus and terms are well-typed (thus free of said errors) by construction. This view of types, sometimes called an intrinsic view, aligns naturally with proof theory and is incredibly well suited for mechanization and mathematical treatment.

The objective of this course is to provide an introduction to typed lambda calculi and their denotational semantics by means of well-typed interpreters. We will begin with a simply typed lambda calculus with products and sums, and go on to cover two different extensions of this calculus, one with a monad and another with a box modality.

Bring pen and paper!

Course page

Introduction to Model Checking with PRISM by Oana Andrei (University of Glasgow)

Model checking is an automated technique for verifying whether a system satisfies its requirements by exploring all of its possible behaviours. In this tutorial we will learn how to model systems as transition systems, specify behavioural requirements using temporal logic, and use model checking to verify properties or generate counterexamples when they are violated. We will then explore these ideas in practice using the PRISM model checker, including a brief introduction to probabilistic model checking. Students are welcome to follow along using PRISM (https://prismmodelchecker.org) on their own laptops. This tutorial is suitable for beginners: no prior knowledge of model checking, formal verification or temporal logic is required.

Introduction to Category Theory by Bob Atkey (University of Strathclyde)

Category Theory is a unifying language for describing mathematical structures and has been especially successful with the kinds of mathematical structures that arise in Computer Science. I will motivate the use of Category Theory in Programming Language and Verification research with some examples, covering the basic notions of category, functor, natural transformations, and universal properties.

Contributed Courses

Formal Modelling with Bigraphs by Blair Archibald (University of Glasgow)

Bigraphs are a versatile modelling formalism, originally by Milner, that describes systems in terms of both spatial placement, e.g. a Person within a Room, and non-local linking, e.g. that Person connected via a radio link to a Cell Tower. In this tutorial we explore bigraphs through a practical lense: how do we specify a system with bigraphs, how are bigraphs combined, how do users specify their own rewrite rules (including probabilistic rules), and how can we use bigraphs once they are defined. Students are welcome to follow along using the [BigraphER tool](https://bitbucket.org/uog-bigraph/bigraph-tools). This tutorial is suitable for beginners: No knowledge of category theory needed!

Distributed Systems: A Logical Approach by Jamie Gabbay (Heriot-Watt University)

An algorithm (= protocol) is distributed when it runs across multiple participants, without central control. A good distributed algorithm allows multiple participants to arrive at some common goal, even though there is no central controller, and even though some participants may not be following the protocol, e.g. they may have crashed, or be actively misbehaving.

Distributed protocols are usually specified as small (or not-so-small) imperative programs. In this course I will present an alternative declarative approach, based on logic. This is to traditional approaches as functional programming is to imperative programming: higher level of abstraction, shorter code, simpler proofs.

The rule of thumb is that declarative methods reduce complexity by a factor of 10 (10x shorter code; 10x shorter proofs). This means that a protocol that took 10 pages of specification and 100 pages of proof in imperative style, in declarative style takes 1 page of specification and 5-10 pages of proof. This is not a projection, it is from a real example.

My approach has been battle-tested on a proposed industrial protocol. It was studied using declarative methods and shown to be incorrect. Using the same declarative methods, the error was fixed. This fix involved nontrivial changes to the basic conceptual structure of the protocol, which were relatively straightforward to see in declarative style but were not evident in the imperative presentation.

In this course, I will give an overview of these methods, starting with simple protocols like Bracha Broadcast and Crusader Agreement, then moving to Paxos and, time permitting, the industrial protocol.

If you want to get a feel for the style of these techniques, you can look at the following resources:

Bracha Broadcast / Crusader Agreement: "Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies" https://arxiv.org/pdf/2512.21137 (in press with Journal of Applied Logics). A Lean formalisation of the proofs is at https://github.com/janmasrovira/mlda
Paxos: "A declarative approach to specifying distributed algorithms using three-valued modal logic" https://arxiv.org/pdf/2502.00892 (submitted)
The industrial protocol: "Heterogeneous trust in reliable broadcast via modal logic and history structures" https://zenodo.org/records/17636313 (submitted). A Lean formalisation of the proofs is at https://doi.org/10.5281/zenodo.17611735

For light reading see also:

"Decentralised collaborative action: cryptoeconomics in space" https://arxiv.org/pdf/2504.12493
A toy model-checking tool, implementing many of these ideas, is at https://github.com/bellissimogiorno/declarative-protocols

Fixpoint Logics by Clemens Kupke (University of Strathclyde)

Modal Logics are used to reason about the finite behaviour of state-based dynamical systems. To be able to express properties of the ongoing, possibly infinite behaviour, one adds fixpoint operators to the logics. This class will explain the fundamentals of how this is done. The content is structured in the following three parts:
(i) Intro to Modal and Temporal Logics
(ii) Fixpoints and their Game characterisation
(iii) A very brief intro to the modal mu calculus

Algebra and Normalisation by Ohad Kammar (University of Edinburgh)

Normalisation concerns specifying a representative in each equivalence class. It comes up whenever we want to guarantee robustness up-to the equivalence relation. For example, a normalising optimising compiler will produce the same object code when you refactor your source code using the equivalence it normalises by. Advanced type-checkers may accept or reject programs by normalising fragments of their types. Modern partial evaluators take incorporate equational laws before extracting a residual program. The hallmark of modern algebra is representation theorems: characterising a structure such as the set of polynomials as the universal structure among a class of structures of interest. In this course, we will explore the relationship between normalisation and modern algebra. We will start with algebraic expressions and universal algebra, and relate them to normalisation and partial evaluation using multi-sorted equational logic. In the second part of the course, we will turn to normalisation of open-programs through the more advanced second-order algebraic structures. [Course web-page](https://denotational.co.uk/algebra-and-normalisation-splv-2026/)

Resource-constrained compiler construction for functional languages by Wim Vanderbauwhede (University of Glasgow)

In this course we explain how to create a compiler for an expressive statically typed functional language targeting a resource-constrained VM (16K memory, 8-bit instructions) and what the challenges are in doing so. As ultimately the compiler should be able to run on the same VM, it has to be constructed in a resource-constrained way.

The course will deal with the architectural and design choices. I will assume attendants have some knowledge of statically typed functional programming (Haskell, ML) with a Hindley-Milner-like type system, but I do not assume knowledge of compilers.

The main blocks are:

The target language, Funktal, an expressive statically typed functional language, and its design choices
The target platform for the language, the Uxn VM, and its assembly language Uxntal
High-level view of a compiler
How to create a resource-constrained compiler: principles, techniques, structure and design

Highly-Assured Programming Language Design and Implementation using Dependent Types by Jan de Muijnck-Hughes (University of Strathclyde)

Traditionally, designing our programming languages has been a pen-&-paper (LaTeX) exercise to describe syntax, semantics, and proofs that important properties hold. These designs must then be realised in software. However, writing software is challenging and errors will be made. Mechanisation offers a way to reduce design and implementation mistakes by making them both machine checkable. This course provides an introduction to mechanised programming language design using dependent types. We will also explore how the same mechanised proofs lay the foundation for a verified pipeline for type-checking and executing programs. No prior experience with dependently-typed programming is required; ample reference material will be provided!

Timetable

Time	Monday	Tuesday	Wednesday	Thursday	Friday
09:00 - 09:30	Registration	Nachi	Jamie	Jan	Oana
09:30 - 10:00	Bob	Nachi	Jamie	Jan	Oana
10:00 - 10:30	Bob	Ohad	Bob	Ohad	Nachi
10:30 - 11:00	Wim	Ohad	Bob	Ohad	Nachi
11:00 - 11:30	Wim	Coffee	Coffee	Coffee	Coffee
11:30 - 12:00	Coffee	Wim	Jan	Bob	Blair
12:00 - 12:30	Nachi	Wim	Jan	Bob	Blair
12:30 - 13:00	Nachi	Lunch	Lunch	Lunch	Lunch
13:00 - 13:30	Lunch	Lunch	Lunch	Lunch	Lunch
13:30 - 14:00	Lunch	Jamie	Clemens	Jamie	Clemens
14:00 - 14:30	Oana	Jamie	Clemens	Jamie	Clemens
14:30 - 15:00	Oana	Oana	(Free)	Clemens	Ohad
15:00 - 15:30	Coffee	Oana		Clemens	Ohad
15:30 - 16:00	Wim	Coffee		Coffee
16:00 - 16:30	Wim	Jan		Blair
16:30 - 17:00	Blair	Jan		Blair
17:00 - 17:30	Blair

Evening		Reception	Dinner

Target Audience

The school is aimed at PhD students in programming languages, verification and related areas. Researchers and practitioners are welcome, as are strong undergraduate and masters students with the support of a supervisor. Participants should have a background in computer science, mathematics or a related discipline. Prospective students may contact the organisers if they have any concerns about background knowledge.