Please register for the SPLS meeting here. The main purpose of the registration is to allow us to estimate the number of participants.
The talks will be delivered via Jitsi and they will also be livestreamed to the SPLS YouTube channel. The link to the Jitsi meeting will be posted to the SPLS Zulip.
The questions after each talk may be asked directly using audio on Jitsi or via the #spls202110 stream on Zulip. Each talk will be preassigned its own separate topic in the Zulip stream.
Breaks and the virtual pub session will take place in the SPLS bar on gather.town. The link to the room will be posted on the Jitsi chat and the SPLS Zulip.
Time  Speaker  Title 

10:0011:00  Tarmo Uustalu 
List monads
We tend to speak of the (possibly empty) list monad and the nonempty list monad, meaning the free monoid monad and the free semigroup monad, as if those were the only monad structures on the list and nonempty list endofunctors (on Set). But they are not! It may at first seem hard to construct other list and nonempty list monads, but at a closer look it turns out that examples abound. There are infinitely many list monads with the singleton function as the unit that admit a presentation with one nullary and one binary operation, and infinitely many nonempty list monads with singleton as the unit and a presentation with one binary operation; some multiplications not only delete, but even duplicate and permute elements. There are list and nonempty list monads with singleton as the unit that have no finite presentation. There are nonempty list monads whose unit is the doubleton function. You cannot tell if a nonempty list monad presented to you as a blackbox is the free semigroup monad by testing the unit and multiplication on finitely many inputs. Etc. We are far from having classified all list monads or all nonempty list monads, but these are cool combinatorial problems. This is joint work with Dylan McDermott and Maciej Piróg. 
11:0011:30  COFFEE BREAK  
11:3012:00  Daniel Hillerström 
Typed Continuations in Wasm
In this talk I will discuss the design and status of the "typed continuations" proposal for Wasm. Nonlocal control flow features provide the ability to suspend the current execution context and later resume it. Many industrialstrength programming languages feature a wealth of nonlocal control flow features such as async/await, coroutines, generators/iterators, effect handlers, call/cc, and so forth. For some programming languages nonlocal control flow is central to their identity, meaning that they rely on nonlocal control flow for efficiency, e.g. to support massively scalable concurrency. Currently, Wasm lacks support for implementing such features directly and efficiently without a circuitous global transformation of source programs on the producer side. One possible strategy is to add special support for each individual nonlocal control flow feature to Wasm, but strategy does not scale to the next 700 nonlocal control flow features. Instead, the goal of this proposal is to introduce a unified structured mechanism based Plotkin and Pretnar's effect handlers which is sufficiently general to cover present usecases as well as being forwards compatible with future usecases, whilst admitting efficient implementations. Proposal repository https://github.com/effecthandlers/wasmspec . 
12:0012:30  Chris Brown 
ProofCarrying Refactorings: Proving Renaming for Haskell via
Dependent Types
Refactoring is the process of changing the structure of a program without changing its behaviour, and is a common practice aimed at making a program more understandable, accessible, or amenable to further alterations to a program's design. Refactorings can be applied manually, which is both a tedious and errorprone process, or via automated refactoring tools, which can both simplify the workflow and guard against common human mistakes, such as overlooking one file within hundreds. Unfortunately, automated tools have their own mode of failure: i.e. changing the behaviour of the code silently in unexpected ways. As refactoring tools grow in power and are applied to ever larger codebases, the key correctness criteria that they indeed do not change program behaviour becomes crucial. Most available refactoring tools do not come with any correctness promises. With common refactoring tools such as Eclipse for Java having wellreported bugs. Indeed, any correctness guarantees of such tools is usually in writing: either by test cases or by handwritten or mechanised correctness proofs. In this talk I will demonstrate a different approach: producing a proof of correctness together with the refactoring, where I use Idris to provide a verified refactoring tool for a subset of Haskell 98. Dependent types provides an implementation of a formally verified semantics of the refactorings and give soundness proofs as part of the refactoring implementations themselves. I will present PART, a Proof Carrying Refactoring Tool for Haskell 98 programs implemented in Idris. I will also give a verified static semantics for a subset of Haskell 98, and a renaming refactoring over that subset. I will conclude with a soundness proof of our renaming implementation. 
12:3014:00  LUNCH  
14:0014:30  Ohad Kammar 
Frex: dependentlytyped algebraic simplification
(joint work with Guillaume Allais, Edwin Brady, Nathan Corbyn, and Jeremy Yallop) I'll present an extensible, mathematicallystructured algebraic simplification library design. We structure the library using universal algebraic concepts: a free algebra; and a free extension  frex  of an algebra by a set of variables. The latter concept, the frex, generalises the `ring of polynomials over a ring' to that of `an algebra of polynomials over an algebra`. The library's dependentlytyped API guarantees that the simplification modules in the library, even userdefined ones, are terminating, sound, and complete with respect to a wellspecified class of equations. Our design is modular in two axes. First, simplification modules share thousands of lines of infrastructure code dealing with termrepresentation, prettyprinting, certification, and macros/reflection. Second, more advanced simplification modules can reuse existing simplification modules. We demonstrate this design by developing three monoid simplification modules: ordinary, commutative, and involutive monoids. We implemented this design in the new Idris2 dependentlytyped programming language, and in Agda. I will demonstrate the Idris2 implementation. 
14:3015:00  Malin Altenmüller 
Decorated Trees
I will present some work in progress towards programming with overconnected data structures. Graphs, for example, can be represented as decorated trees: their spanning tree together with some additional edges. The structures of our current interest are planar graphs, where no edges cross. For implementing operations like navigating to a different place within a graph, we use some well known techniques on the underlying tree, while ensuring that the decoration stays in place. More interesting questions include the choice of spanning tree, rerooting a tree and views from different positions. This is joint work with Conor McBride. 
15:0015:30  Hossein Haeri 
Mind Your Outcomes  QualityCentric Systems Development in a Pure
Functional Framework
This paper defines the ΔQ𝑆𝐷 language that embodies the main concepts of the ΔQ framework for distributed systems design. The ΔQ framework has been developed over three decades to design large distributed systems with predictable behaviour under high applied load. The framework specifies system designs at different levels of refinement and tracks and predicts their performance envelope as a function of load. System designers can thereby determine whether the system is likely to perform satisfactorily before the system is actually built. This is a critical property for realworld systems: they are expected to perform well in exactly those cases when it is difficult to ensure adequate performance, such as telephony systems during natural catastrophes. The ΔQ𝑆𝐷 language defines a system as a formal structure (called an “outcome diagram”) that makes explicit how all system behaviours relate to each other. The system’s design is then a sequence of refinement steps starting from a system with wholly unspecified structure and ending with a system with completely specified structure. We give the language semantics that allows computation of the predicted system performance at any step in the refinement process. In future work we intend to incorporate ΔQ𝑆𝐷 in software tools and to use it to provide formal proofs that a partially specified design’s performance is adequate or inadequate. This will make it a practical and useful tool for system designers. 
15:3016:00  COFFEE BREAK  
16:0016:30  Matthew Daggitt 
Embedding constraints in neural networks: from training to termination
In the last 5 years the pressing need to ensure the safety of AI systems has led to the development of a plethora of different tools targeting the problem of how to constrain the relationship between a neural network's inputs and outputs. This includes: training it to obey the relationship, verifying the relationship holds or finding counterexamples, and verifying larger systems that make use of the network. In this talk I will describe how our proposed DSL Vehicle, aims to bridge the gaps between all these different tools and provide a single highlevel human readable interface for embedding and monitoring the properties of a network all the way through its lifecycle. 
16:3017:00  André Videla and Matteo Capucci 
Parametrised lenses and clientserver relationships
Parametrised optics form the backbone of categorical cybernetics [1], an area of study focused on interactive, controlled systems. The central mathematical innovation is acknowledging the Para construction as the way to talk about controlledcontroller relations in cybernetic systems while retaining a straightforward graphical calculus and mathematical theory. Applications of this framework include open games (compositional game theory [1, 2]) and open learners (compositional machine learning [1, 3]). In this presentation we show how common clientserver relationships (such as CRUD/RESTful APIs) can be treated in the same fashion. We propose parametrised lenses as an expressive primitive for a server library, allowing programmer to write and extend clients and servers without the hassle associated with it. The talk will feature both a categorical and theoretic analysis and a walkthrough of an Idris implementation of a RESTful server library. This presentation is a follow up from the existing talk “Optics for servers” [4]
References:

17:30???  Virtual Pub 