| title | custom_css | speciala | specialb | specialc | core1 | core2 | invited | lightning | |||
|---|---|---|---|---|---|---|---|---|---|---|---|
SPLV 2024 |
|
Vikraman <sup>MC319</sup> | Andrés <sup>MC301</sup> |
Bob <sup>MC301</sup> | Sam <sup>MC319</sup> |
Kathrin <sup>MC301</sup> | Jules <sup>MC319</sup> |
Conor <sup>MC301</sup> |
Chris <sup>MC301</sup> |
Jean-Marie <sup>MC301</sup> |
<a href="lightning.html">Lightning</a> |
University of Strathclyde, Glasgow, UK — July 29th to August 2nd
{% include_relative menu.html %}
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.
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 | {{page.core1}} | {{page.core2}} | {{page.speciala}} | {{page.specialb}} | |
| 09:30 | |||||
| 10:00 | {{page.core1}} | {{page.specialc}} | {{page.speciala}} | ||
| 10:30 | {{page.specialb}} | ||||
| 11:00 | {{page.core2}} | ||||
| 11:30 | {{page.invited}} | {{page.invited}} | {{page.invited}} | {{page.invited}} | |
| 12:00 | |||||
| 12:30 | |||||
| 13:00 | |||||
| 13:30 | {{page.core1}} | {{page.speciala}} | {{page.specialb}} | {{page.specialc}} | |
| 14:00 | |||||
| 14:30 | {{page.specialb}} | {{page.specialc}} | |||
| 15:00 | |||||
| 15:30 | {{page.core2}} | ||||
| 16:00 | {{page.specialc}} | {{page.speciala}} | |||
| 16:30 | |||||
| 17:00 | {{page.lightning}} | {{page.lightning}} | |||
| 17:30 | |||||
| 18:00 | |||||
| 18:30 | |||||
| 19:00 | |||||
| 19:30 | |||||
| 20:00 | |||||
| 20:30 |
These required lectures cover foundational knowledge.
Category Theory
: Lecturer: Chris Heunen
**Slides:** [Monday and Tuesday combined](assets/slides/chris.pdf)
:
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](assets/slides/conor.pdf), [Agda code](https://github.com/pigworker/TypesWhoSayNi/tree/master/spls)
:
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.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](https://users.soe.ucsc.edu/~lkuper/)
: 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.The specialised courses are offered as two tracks running in parallel.
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.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
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 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.
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.
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.
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.
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:
- Guillaume Allais [email protected]
- Fredrik Nordvall Forsberg [email protected]
- Jan de Muijnck-Hughes [email protected]
- Sean Watters [email protected]