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.

Last Day

On the last day, we will be in Sir Alwyn Williams Building room 422/423. There are signposts once you get into the building, make your way to floor 4.

Venue

Courses held on Monday - Thursday will be held in One A, The Square. You can enter through the main building entrance (signposted as the Gilchrist), and then follow signs for SPLV. A detailed campus map is available here.

Arrangements for Friday

On Friday, the summer school will be held in School of Computer Science itself, in the Sir Alwyn Williams building. We will be in room SAWB 422/423, which can be found on floor 4. The organisers will be around in the morning to help you find your way, and it will be clearly signposted.

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. To get here, please go to the main gates. We will make sure that the venue is signposted and members of the organisation team will be there to help on the day. Registration will be open 9-9:30AM on Monday 3rd July; if you arrive later please just talk to an organiser and we will get you your badge. There is no need to print out your ticket; we will have a list of all participants.

Accommodation

If you have booked accommodation, this is at Queen Margaret Residences. Keys can be collected from the main reception in the Queen Margaret Residences Central Services Building from 2.00 pm on Sunday 2nd August. The site is staffed 24 hours a day, and security can assist with key collection outside normal reception hours. Check-out is by 10.00am on Friday 7th August.

Zulip

Feel free to join our Zulip!

Social Programme

Pub Quiz

We have organised a pub quiz on Monday evening. This will take place upstairs in curlers rest. The quiz will start from (about) 7PM - feel free to take your time wandering down.

City Chambers Reception

For the Tuesday evening, We have organised a drinks reception with the lord provost. This will be held at Glasgow City Chambers, from 6PM. The organisers will lead groups across, so you are welcome to follow us. If you want to make your own way, we recommend taking the subway. Hillhead is the closest station to campus; you would need to get off at Buchanan street. The city chambers are a short (5 minute) walk from there.

Conference Dinner

We have organised a conference dinner for the wednesday evening at Òran Mór. Doors open at 6:45PM, which should give you plenty of time to find a seat. Food will be served from (about) 7PM and there is a bar available throughout the evening where drinks can be purchased.

Registration and Accommodation

Registration is now open via Eventbrite.

Registration is priced as:

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:

  1. 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
  2. Paxos: "A declarative approach to specifying distributed algorithms using three-valued modal logic" https://arxiv.org/pdf/2502.00892 (submitted)
  3. 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:

  1. "Decentralised collaborative action: cryptoeconomics in space" https://arxiv.org/pdf/2504.12493
  2. 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
10:00 - 10:30 Ohad Bob Ohad Nachi
10:30 - 11:00 Wim
11:00 - 11:30 Coffee Coffee Coffee Coffee
11:30 - 12:00 Coffee Wim Jan Bob Blair
12:00 - 12:30 Nachi
12:30 - 13:00 Lunch Lunch Lunch Lunch
13:00 - 13:30 Lunch
13:30 - 14:00 Jamie Clemens Jamie Clemens
14:00 - 14:30 Oana
14:30 - 15:00 Oana (Free) Clemens Ohad
15:00 - 15:30 Coffee
15:30 - 16:00 Wim Coffee Coffee
16:00 - 16:30 Jan Blair
16:30 - 17:00 Blair
17:00 - 17:30
Evening

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.

Contact

You can reach the organisers at:

glasgow-splv-organisers@lists.cent.gla.ac.uk

The organisers of SPLV’26 are:

Sponsors

Gold Sponsors

ACM SIGPLAN

Amazon Web Services

Silver Sponsors

Jane Street

Bronze Sponsors

Well-Typed

This site is open source. Improve this page.