| title | custom_css |
|---|---|
SPLS, 22 November 2023, University of Strathclyde |
custom |
The Scottish Programming Languages Seminar (SPLS) Series is an informal meeting of the Scottish Programming Languages Institute (SPLI) Community for discussing anything related to programming languages.
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.
We kindly acknowledge the continuing sponsorship of the Scottish Informatics and Computer Science Alliance (SICSA).
- 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 2023 here.
- Registration is required for catering.
- 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.
In-person event for PhD students in MC316.
|
| 13:00—13:30 | Ross Horne (University of Strathclyde) |
Reasoning about Privacy using Bisimilarity Congruences
(Video)
Hide Abstract
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. |
| 13:30—14:00 | Danel Ahman (University of Ljubljana, Slovenia) |
When programs have to watch paint dry
(Video)
Hide Abstract
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. |
| 14:30—15:00 | Vikraman Choudhury (University of Glasgow) |
An abstract look at commutativity
(Video)
Hide Abstract
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
Hide Abstract
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. |
| 15:30—16:00 | Joseph Eremondi (University of Edinburgh) |
Coverage Semantics for Dependent Pattern Matching
(Video)
Hide Abstract
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. |
| 16:30—17:00 | Cristina Matache (University of Edinburgh) |
Scoped effects as parameterized algebraic theories
Hide Abstract
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)
Hide Abstract
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. |
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.
The McCance Building on the map (larger version):
Should you have comments or queries about the event please contact one of the organisers:
- Principal: Riu Rodríguez Sakamoto <riu.rodriguez-sakamoto AT strath DOT ac DOT uk>, Dilsat Yuksel <dilsat.yuksel AT strath DOT ac DOT uk>
- Junior: Jan de Muijnck-Hughes, Fredrik Nordvall Forsberg
- Chairs: Ezra Schoen (Session 1), Malin Altenmüller (Session 2), James Wood (Session 3)