| title | custom_css | |
|---|---|---|
SPLV 2025 |
|
This year, the Scottish Programming Languages and Verification Summer School will be held at The University of Edinburgh.
For announcements and updates concerning SPLV 2025, please subscribe to our SPLS Zulip stream.
Program verification using concurrent separation logic (guest course)
: Guest Lecturer: Robbert Krebbers, Radboud
University Nijmegen
:
Abstract
Concurrent programs are challenging to get right, especially if threads share access to memory. The formalism of "concurrent separation Logic" (which was pioneered by O'Hearn and Brookes in 2007) provides a powerful framework to verify concurrent programs. Over the last 20 years, concurrent separation Logic has emerged into an active research field, has been extended with many features (e.g., fine-grained concurrency, weak memory consistency, higher-order programs), been applied to many programming languages (e.g., Rust), and has been implemented in numerous verification tools (e.g., F*, Iris, Verifast, Viper, VST). We will discuss the foundations of separation logic and show how they scale to the verification of challenging concurrent programs. Exercises and demos using the Iris framework in the Rocq proof assistant will be provided.A few ideas from distributed systems for PL folk (guest course)
: Guest Lecturer: Lindsey Kuper,
University of California, Santa Cruz
:
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.Application programming with dependent types
: Lecturer: Edwin Brady,
University of St Andrews
:
Abstract
TBDType theory
: Lecturer: Fredrik Nordvall Forsberg, University
of Strathclyde
:
Abstract
Type theory is both a foundation of mathematics and an expressive functional programming language, and the basis of proof assistants and programming languages such as Agda, Idris, Rocq, and Lean. There are many aspects to type theory, and these lectures will give an introduction to three of them: (i) what it is, and how to work in it (the user's perspective); (ii) studying type theory as a formal system, and proving properties such as normalisation, canonicity, and subject reduction (the metatheorist's perspective); and (iii) models of type theory, and how they suggest new axioms, as well as let us conveniently manipulate mathematical structures of interest (the semanticist's perspective).Behavioural types
: Lecturer: Simon Fowler, University of
Glasgow
:
Abstract
Much like data types allow us to rule out common programming errors before we compile or run a program, behavioural type systems provide a lightweight way of checking the correctness of behavioural properties of programs. Three examples include typestate, which allows us to ensure that we call object methods in the correct order (e.g. opening a file handle for reading before performing read operations and eventually closing the handle); session types, which allow us to check that a communication follows a protocol; and mailbox types, which allow us to specify patterns of messages received in many-to-one communication. This course will give an overview of behavioural typing, going into depth on the theoretical and practical aspects of session types and mailbox types.Concurrency theory
: Lecturer: Rob van Glabbeek, University
of Edinburgh
:
Abstract
This course aims to make students familiar with state-of-the-art techniques in modelling concurrent systems. This is done by comparing some of the more successful semantic models of concurrency found in the literature, including transition systems, Petri nets and process algebras. The focus will be on the rationale behind the design decisions underlying those models, viewed from philosophical, mathematical and computational perspectives. A central concept will be that of a semantic equivalence or preorder, relating system specifications and implementations.Logical relations for program equivalence
: Lecturer: Filip Sieczkowski,
Heriot-Watt University
:
Abstract
In this course we will explore logical relations, as a classic type-based method of proving equivalence of programs and, crucially, program fragments. We will introduce the problem of program (fragment) equivalence and solve it in the setting of simply-typed lambda calculus, and proceed to extend the method to some of the features found in modern programming languages, including polymorphism, recursion in types and terms, and computational effects, ending with a look at extending the methodology to type-and-effect systems.Models, programs and bidirectional transformations
: Lecturer: Perdita Stevens, University of
Edinburgh
:
Abstract
Historically there has - surprisingly, perhaps - been something of a gulf between the programming languages and software engineering communities, which I will argue has been to the detriment of both. One of the many places this shows up is in the fields' treatments of bidirectional transformations, by which I mean, automated means of checking and restoring appropriate notions of consistency between data sources. I will introduce this topic from a software engineering perspective, which will necessitate introducing modelling and model-driven engineering more generally. I will briefly wave at the treatment of the topic in the functional programming community, via optics. I will opine about some open problems and some things I think the next generation of researchers should pay attention to, in order to narrow rather than widen the gulf between PL and SE, to the benefit of both.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.
We are happy to be able to offer some financial support for attendees.
EuroProofNet:
Participants from Inclusiveness Target Countries* (ITC) can apply with EuroProofNet for funding towards travel and accommodation. The reimbursment rules can be found on the EPN website. Please contact Frédéric Blanqui to apply.
(*) list of ITC countries: Albania, Armenia, Bosnia and Herzegovina, Bulgaria, Croatia, Cyprus, Czech Republic, Estonia, Georgia, Greece, Hungary, Latvia, Lithuania, Malta, Moldova, Montenegro, North Macedonia, Poland, Portugal, Romania, Serbia, Slovakia, Slovenia, Turkey, Ukraine.
Support for PhD Students:
We will be able to subsidise student participation. Details about scholarships will appear here.
The summer school is generously supported by the following sponsors:
If you have any questions please get in contact with the local organising team at:
The principal organisers of SPLV25 are:
- Malin Altenmüller [email protected]
- Ohad Kammar [email protected]
- Sam Lindley [email protected]
- Nachi Valliappan [email protected]