SPLS Glasgow 1st July 2022

The Scottish Programming Languages Seminar (SPLS) is an informal seminar for discussing anything PL related. This edition will be held both in-person and online. The in-person meeting will be on Level 4, Sir Alwyn Williams Building, University of Glasgow.

This edition of SPLS is sponsored by SICSA.

Scottish Informatics & Computer Science Alliance


If you would like to attend physically, please register on the Doodle.

There is no need to register if you would like to attend online. Information on how the seminar will be streamed is coming soon.


Following Scottish Government and University guidance, we ask participants displaying potential COVID-19 symptoms not to attend physically, and encourage participants to wear masks in indoor areas should they become busy. The University supports the Distance Aware scheme, and can provide appropriate lanyards and badges.

We strongly encourage participants to take a Lateral Flow Test (LFT) prior to the event; although the national testing programme has now finished, LFTs can be purchased from most major supermarkets and pharmacies.


The following is a tentative schedule for this edition of SPLS. Note that the call for lightning talks is currently open, feel free to get in touch to give a short 5-10min talk about ongoing work.


12:00-13:00 Lunch
13:00-14:00 Session: Semantics Chair: Simon Fowler
13:00-13:30 Bruce Collie The K Framework: Practical Semantic Tools from Term Rewriting
13:30-14:00 Nachiappan Valiappan Normalization for Fitch-style Modal Calculi
14:00-14:30 Coffee
14:30-15:30 Session: Type Systems Chair: Matthew Alan Le Brun
14:30-15:00 Katarzyna Marek Idris-TyRE - a Dependently-Typed Regex Parser
15:00-15:30 Conor McBride TypOS: An Operating System for Typechecking Actors
15:30-16:00 Coffee
16:00-17:00 Session: Refactoring and Lightning Talks Chair: Jeremy Singer
16:00-16:30 Chris Brown RePi: Towards a Refactoring Tool for Dependently Typed Programs
16:30-17:00 Lightning Talks
Stefan Marr (remote) Job opportunities at Kent
Vashti Galpin (remote) Temporal Links for Data Curation
Matthew Alan Le Brun Towards Fault-Tolerant Session Types: A Calculus for Distributed Computing
Daniel Hillerström WasmFX: Effect Handlers for WebAssembly


Bruce Collie The K Framework: Practical Semantic Tools from Term Rewriting
K (https://kframework.org/) is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined. From a single language definition in K, an entire suite of tools can be automatically derived (including a parser, concrete interpreter, and symbolic execution engine); it provides a flexible, powerful environment for constructing programming languages. In this talk, I'll provide an introduction to K by demonstrating a simple imperative language semantics, along with a set of proofs over programs in this language enabled by K's generic theorem prover. Finally, I'll talk briefly about how we use K commercially at scale in the blockchain and embedded software domains.
Nachiappan Valiappan Normalization for Fitch-style Modal Calculi

Fitch-style modal lambda calculi enable programming with necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator that is denoted by a lock. The addition of locks simplifies the formulation of typing rules for calculi that incorporate different modal axioms, but each variant demands different, tedious and seemingly ad hoc syntactic lemmas to prove normalization. In this work, we develop normalization by evaluation (NbE) for Fitch-style calculi that incorporate the K, T and 4 axioms of modal logic by leveraging their possible-world semantics. The NbE approach exploits the commonalities of these calculi in the possible-world semantics and isolates their differences to a specific parameter that determines the modal fragment, thus enabling reuse of the evaluation machinery and many lemmas proved in the process. Finally, we showcase several consequences of normalization for proving meta-theoretic properties of Fitch-style calculi based on different interpretations of the necessity modality in programming languages, such as capability safety, noninterference and a form of binding-time correctness.

Paper and mechanization available here.

Katarzyna Marek Idris-TyRE - a Dependently-Typed Regex Parser
Regexes are widely used not only for validating, but also for parsing textual data. Generally, regex parsers output a very generic structure, e.g. an unstructured list of matches, leaving it up to the user to validate the output's properties and transform it into the desired structure. Since the regex itself carries information about the structure, this leads to unnecessary repetition. In this talk we will present Idris-TyRE - a library for type-driven regex parsing. The idea is based on Radanne’s typed regexes library of the same name - a typed, indexed combinators layer that can be added on top of an existing regex engine. In contrast to Radanne's design, we also implement a parser, which maintains the type-safety throughout all layers. The parser is implemented in Idris 2 utilising the following features of Idris 2's advanced type system. We take advantage of type-level computation to establish the correct parse tree type; we use dependent-type verification to ensure the result type correctness; and we benefit from quantitative types by erasing the proofs and avoiding run-time overhead. This is joint work with Ohad Kammar.
Conor McBride TypOS: An Operating System for Typechecking Actors

TypOS is an experimental language specific to the domain of implementing type checking, type synthesis and type-directed elaboration algorithms, presented as concurrent actors. We develop the idea "A rule is a server for its conclusion and a client for its premises." into a framework where the judgment forms are presented as interaction protocols and the rules for a given judgment are collectively presented as an actor serving the judgment's protocol. A running actor may spawn new actors of which it is the client, each with its own channel. The parameters to each judgement thus acquire not only a syntactic category, but also a mode as input or output. With this stromger sense of information flow, the language of formulae occurring in rules naturally splits into patterns which analyse things coming and expressions which synthesize things going. Expressions may contain substitutions to be done, but patterns may not, because substitutions are hard to undo. More generally, the TypOS design strategy is to prevent practices likely to result in failure of metatheoretical safety properties. We pay particular attention to term variable scope, for example ensuring that no actor can learn the name of a variable bound by another. TypOS also supports the speculation of unknowns, which become monotonically more defined as constraints are solved: we thus have the one kind of shared memory that makes sense in a distributed setting. Actors can thus block if they need information which is not yet available: ensuring that resuming actors operate on up-to-date information is the implementation challenge which precipitated the whole effort.

TypOS is joint work with Guillaume Allais, Malin Altenmueller, Georgi Nakov, Fredrik Nordvall Forsberg and Craig Roy. GitHub repository.

Chris Brown RePi: Towards a Refactoring Tool for Dependently Typed Programs

Dependently-typed programming languages are becoming increasingly popular in the functional programming community, allowing programmers to express properties of logic and proofs as part of their implementation. Dependent types permit the programmer to implement safe programs, by encoding safety properties as parts of the types themselves; these properties can be encoded by permitting the types to depend on values. However, programming dependently-typed systems is still very difficult for the average software developer, who may have had some prior training with functional languages, such as Haskell, but lacks the background and experience in logic and type systems to make appropriate use of the dependent types to build strong safe systems as a part of their day-to-day practice.

Refactoring aims to provide programmers with the ability to systemically restructure their code to better reflect its purpose, making it more amenable to change and maintainability, or simply to make it more understandable. The advantage of refactoring tool support is that it not only presents the programmer with a structured set of well-defined transformations, but it also alleviates the error-prone burden of manually making modifications across an entire project that might contain thousands of source code modules. To date, however, there are no refactoring tools for dependently-typed programming languages.

In this talk, we address this problem by discussing a number of new refactorings to be implemented for the dependently-typed programming language, Pi-Forall, developed by Weirich. We particularly focus on refactorings for extending and maintaining data types in Pi-Forall. We demonstrate our prototype refactorings over a simple lambda calculus example and discuss our preliminary refactoring tool, RePi.


The organisers of this edition of SPLS are Jeremy Singer, Matthew Alan Le Brun and Simon Fowler. Feel free to contact any of the organisers about queries regarding this seminar.