This edition of SPLS will be hybrid and is organised by the MSP Group of the Department of Computer & Information Sciences at University of Strathclyde.
We will be physically located in the McCance Building, room MC301 at the University of Strathclyde for the main event.
Note that the PhD Event in the morning will be held in room MC316.
Accessibility information is available here.
For online participants we will stream the talks using YouTube.
If you plan to attend in person register by the 8th November 2023 using this form.
If you wish to give a talk then please indicate it in the above form. If your title or abstract is yet to be determined, they can be sent by the 15th November 2023 per email to one of the organizers.
If you want to attend the morning PhD event, please also fill in your name by the 8th November 2023here.
Registration is required for catering.
COVID Information
There are no COVID restrictions on attendance, however, we welcome mask wearing in packed indoor areas as well as testing on the morning prior to attending.
Programme
10:00—12:00 PhD EVENT (MC316)
In-person event for PhD students in MC316.
10:00 - 10:30 Coffee and welcome
10:30 - 11:30 University and SPLI presentation
11:30 - 12:00 Live Q&A
12:00—13:00 Lunch (MC301)
13:00—14:00 Session 1: Behaviour (MC301)
13:00—13:30
Ross Horne (University of Strathclyde)
Reasoning about Privacy using Bisimilarity Congruences
(Video)
Privacy problems such as unlinkability (the inability of an attacker to link two sessions involving the same agent) can be expressed as an equivalence problem (c.f. Arapinis et al.). This formulation of unlinkability has been a stimulator for all sorts of problems in the foundations of concurrency theory, in logic, and other aspects of symbolic reasoning that feed into tool support for verification; with nuances guided strongly by problems arising in the design of privacy-preserving protocols. I'll provide a brief overview of a few guiding protocol problems mainly concerning privacy-preserving smartcards (inviting the listener to elaborate on those that interest them). However, I'll zoom in on a neat observation that some protocols can exploit compositional reasoning to reduce the size of proofs and simplify their structure when verifying unlinkability problems. This is done by employing a suitable congruence as the notion of equivalence, where the equivalence also reflects a realistic threat model.
In this talk I will discuss how one can use types and effect systems to modularly specify and check when programs are allowed to use their resources, e.g., when programming a robot arm on a production line, it is crucial that painted parts are given enough time to dry before assembly. In particular, I will show how an effectful λ-calculus based on a time-graded variant of Fitch-style modal types allows one to capture such temporal resources. Importantly, waiting for resources to become available does not necessarily have to be spent idly looking around, but the programs can instead do other useful work.
A neat feature of the calculus is that it includes a temporally aware variant of graded algebraic effects and effect handlers. The former are given a novel temporal treatment in which operations' continuations know that an operation's worth of additional time has passed before they resume execution, making it possible to safely access further temporal resources in them, and where effect handlers have to respect this temporal discipline. I will also discuss a presheaves-based denotational semantics and a stateful operational semantics for this calculus (the latter is joint work with Gašper Žajdela).
Lists as free monoids are a well-known construction in type theory. Adding the commutativity axiom to monoids makes things unpleasant. In this talk, I will show how to go from free monoids to free commutative monoids, working in univalent type theory. I will discuss various constructions of free commutative monoids, and the abstract properties they satisfy. I will show implementations and applications of these ideas in Cubical Agda.
15:00—15:30
Anton Lorenzen (University of Edinburgh)
The Functional Essence of Imperative Binary Search Trees
Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts; yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanised the proofs establishing this in the Coq proof assistant using the Iris framework.
This yields a first fully verified implementation of well known algorithms on binary search trees.
15:30—16:00
Joseph Eremondi (University of Edinburgh)
Coverage Semantics for Dependent Pattern Matching
(Video)
Dependently-typed systems like Agda and Idris elaborate nested dependent pattern matching to a system of top-level patterns. Semantics for pattern matching is then given via a translation into a core calculus with eliminators: primitive fold-like functions with a one-to-one correspondence between branches and the scrutinee type’s constructors. More sophisticated forms of matching are given semantics indirectly: matches with nested patterns, multiple scrutinees, or impossible cases are elaborated to eliminators.
We propose a direct semantics for top-level dependent pattern matching that avoids this elaboration step. Matching is parameterized over an axiomatic notion of “coverage” that dictates which sets of patterns form a valid left-hand-side for a match, making no assumptions about whether they correspond to constructors for an inductive type. Using the language of sheaf theory, we provide criteria for coverages that are sufficient to give semantics to pattern matching, as well as some techniques for deriving new coverages from old ones.
16:00—16:30 Coffee
16:30—17:30 Session 3: Well-scoped (MC301)
16:30—17:00
Cristina Matache (University of Edinburgh)
Scoped effects as parameterized algebraic theories
This talk is about algebraic theories and effect handlers. Algebraic theories provide a way of axiomatizing computational effects using operations and equations, where operations are basic programming features like reading and updating the state, and equations specify observably equivalent programs. Effect handlers provide a way of implementing effectful operations and of modularly programming with them. I will recall parameterized algebraic theories, a generalization of algebraic theories, and scoped effects, an extension of effect handlers. For example, exception catching which is traditionally not algebraic can be implemented as a scoped operation. I will then argue by example that scoped effects can be axiomatized using parameterized algebraic theories, thus obtaining equational characterizations of existing models of scoped effects.
17:00—17:30
Jan van Brügge (Heriot-Watt University)
A new framework for defining binding-aware datatypes
(Video)
In this talk I present a framework for Isabelle/HOL for defining and reasoning about binding-aware datatypes. Compared to previous frameworks (namely Nominal2), our system has several improvements. First, it allows to nest recursion through other datatypes which greatly improve reuse of existing theorems. The framework also allows to bind through quotients and other non-free datatypes and it generalizes to infinite types/codatatypes. We also identified conditions for improving inductive predicates that involve binders so their induction theorem observes the variable convention.
17:30—late Dinner/Pub
Travel
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.
