SPLS — 11th February 2026 (11:30–17:30)

Formal modeling tools such as Alloy enable users to incrementally define, explore, verify, and diagnose specifications for complex systems. A critical component of these tools is a visualizer that lets users graphically explore generated models. However, a default visualizer that knows nothing about the domain can be unhelpful and can even actively violate presentational and cognitive principles. At the other extreme, full-blown custom visualization requires significant effort as well as knowledge that a tool user might not possess. Custom visualizations can also exhibit bad (even silent) failures. The same needs and demands apply to programming languages, which are virtually never accompanied by data structure visualizers.
We chart a middle ground between the extremes of default and fully-customizable visualization. We capture essential domain information for lightweight diagramming. To identify key elements of these diagrams, we ground the design in both cognitive science and in a corpus of custom visualizations. We distill from these sources a small set of orthogonal primitives, and use the primitives to guide a diagramming language.
We show how to endow the diagramming language with a spatial semantics and prove that it enjoys key properties. We also show how it can be embedded into three very different languages: Python, Rust, and Pyret. We present a novel counterfactual debugging aid for diagramming errors, combining textual and visual output. We evaluate the language and system for expressiveness, performance, and diagnostic quality. We thus define a new point in the design space of diagramming: through a language that is lightweight, effective, and driven by cognitively sound principles.

Probabilistic programming languages (PPLs) are a useful tool for statistical modelling, and semantics of PPLs are a highly active field of research. In the literature, two main approaches to give semantics to PPLs have emerged: Semantics based on categories of linear operators and semantics based on categories of Markov kernels, where a Markov kernel is a generalisation of a stochastic matrix. Both approaches have its strengths and weaknesses, and its weaknesses are complementary. Addressing these weaknesses is, traditionally, both highly technical and subtle.
Recent advance has been achieved by Azevedo de Amorim who defines a two-level calculus nicely combining both types of PPLs: One level can be interpreted by categories of linear operators and the other one using categories of Markov kernels, while a modality mediates between both levels, which is interpreted by a lax monoidal functor. We introduce the term Banach category to refer to models of this calculus.
Azevedo de Amorim's PPL has already been applied in the literature, but the theory of Banach categories remains underdeveloped, an issue we address in this work: Azevedo de Amorim points out that the semantics of his calculus behave even better when the lax monoidal functor is full, motivating us to prove our main theorem: Subject to certain conditions, for any Banach category, one can find another Banach category - its fullification - such that the lax monoidal functor of the fullification is full and the original Banach category and its fullification are related in a nice way.
This is joint work with Pedro H. Azevedo de Amorim (Universities of Bath and Oxford) and Ruben van Belle (University of Oxford).

Elaboration allows users of dependently typed programming languages to avoid writing seemingly obvious types and terms and instead focus on the important details of their proofs and programs, so it's implemented in many major dependent type checkers. This talk explains the issues I encountered when extending a basic elaboration algorithm, based on Coquand's bidirectional type checking algorithm and unification, to Multimodal Dependent Type Theory — a type theory that extends Martin Löf Type Theory with modal operators that interact in interesting ways with variables and substitutions.

Program extraction for dependently-typed languages such as Rocq often requires unsafe type casts. In this work I present some early ideas on a language called Extractly. To remove type-casts from extracted Extractly programs, we forbid large elimination of data types and rely on indexed data types (GADTs). Whilst nothing has yet been formalised, I present a "recipe" for removing large elimination which works for all examples I have found. This includes a metacircular interpreter for the simply-typed lambda calculus.

There have been various different attempts to introduce parallel programming models into functional languages, from very implicit approaches, such as the par and pseq model exhibited by GpH, to semi-explicit process models exhibited by the Haskell implementation, Eden, to very explicit actor-based models that use message passing and explicit process creation, such as Erlang. Implicit vs. explicit parallel models introduce important trade-offs to programmers. Explicit models give more control over the parallelism, but require much more low-level management (and often more expertise from the programmer); implicit approaches give less control over the parallelism (and therefore often require less parallel expertise) but offer more reasoning opportunities. However, to date, there has been little exploration to introduce implicit parallelism approaches to an emerging class of dependently typed programming languages.
Dependently typed programming languages, such as Idris, Lean, Agda and Coq, allow programmers to encode specifications of their programs as specialised types that depend on values. This value dependence means that the types express logical relations and the programs provide proof obligations that the relations hold. With the exception of pi-par, an extension to Idris with explicit process creation and message passing, there are little to no parallel dependently-typed languages that offer implicit parallel models to the programmer.
In this talk I introduce a semi-implicit programming model, similar to Eden for Haskell, by extending Idris with a dependently-typed process abstraction. This semi-implicit process model means that processes can be explicitly created, but low-level details, such as communication, synchronisation and scheduling is abstracted away by the runtime. Furthermore, our process model is enhanced by making use of dependent types to allow some of the parallel behaviour to be exposed to the programmer at the type level. In turn, this enables further typing abstractions that describe common parallel patterns and skeletons.

Amortized analysis is a technique for proving a combined time bound for a batch of operations on a data structure, even if some of those operations are expensive.
But the traditional method of amortized analysis yields wrong time bounds when the data structure is used persistently. Persistence allows operations to be performed on previous versions of the data structure, which prevents amortization of expensive restructuring work.
In his seminal work, Chris Okasaki showed how to extend amortized analysis to persistent usage. His method works by storing debits on thunks. However, Okasaki describes his approach only informally, which makes it hard to understand precisely when and why it works.
In my talk, I'll give a formal definition of persistence and show that traditional amortized analysis is not persistent. Then I show that it is possible to perform amortized analysis by storing credits on thunks and that this is persistent.

What is the mathematical structure of debugging? Reversible debuggers allow programmers to record a linear trace of the program's execution, and then interactively step forwards or backwards in time. If the program is concurrent, however, there are interleaved events and causal dependencies between them, and the forward and backward steps need to respect this structure. In this talk, I will describe how this notion of causal-consistent reversibility in concurrent computation can be formalised using event structures. This is joint work with Ivan Lanese.