Stardust meeting at Glasgow
(24th and 25th April 2025)

Location

The meeting will be held on April 24th and 25th, 2025, at the University of Glasgow (Sir Alwyn Williams Building, see map, in rooms 422 and 423). The meeting will be held in-person, with a hybrid session on Friday. In case of problems or further information, contact Simon Fowler.

Thursday 24th April (09:00 - 17:00)

09:00 - 09:30	Arrival and coffee	Outside SAWB 423
09:30 - 11:00	Technical session 1 09:30: Speak Now: Safe Actor Programming with Multiparty Session Types (Simon Fowler, Glasgow) 10:15: Less is More Revisited (Nobuko Yoshida, Oxford)	SAWB 423
11:00 - 11:30	Coffee	Outside SAWB 423
11:30 - 13:00	Technical session 2 11:30: Session Subtyping by Fixpoint Acceleration (Andy King, Kent) 12:15: Non-linear communication via graded modal session types (Danielle Marshall, Glasgow)	SAWB 423
13:00 - 14:00	Lunch	Outside SAWB 423
14:00 - 15:30	Technical session 3 14:00: Partial Probabilistic Multi Party Session Types (Joe Paulus, Oxford) 14:45: Multiparty Session Types with a Bang! (Matthew Alan Le Brun, Glasgow)	SAWB 423
15:30 - 16:00	Coffee	Outside SAWB 423
16:00 - 17:00	Site Reports and discussion	SAWB 423
19:00	Dinner	Cafe Andaluz

Friday 25th April (09:30 - 12:00)

09:30 - 10:00	Coffee	Outside SAWB 422
10:00 - 10:45	Technical session 4 10:00: Mailboxer: Early Detection of Erlang Communication Errors (Duncan Paul Attard, Malta)
10:45 - 11:15	Coffee	Outside SAWB 422
11:15 - 12:00	Technical session 5 11:15: Asynchronous Mixed Choices (A unifying framework for failure handling) (Laura Bocchi, Kent)	SAWB 423
12:00	Closing and lunch

Abstracts

1. Speak Now: Safe Actor Programming with Multiparty Session Types (Simon Fowler, Glasgow)
   Actor languages such as Erlang and Elixir are widely used for implementing scalable and reliable distributed applications, but the informally-specified nature of actor communication patterns leaves systems vulnerable to costly errors such as communication mismatches and deadlocks. Multiparty session types (MPSTs) rule out communication errors early in the development process, but until now, the nature of actor communication has made it difficult for actor languages to benefit from session types. This paper introduces Maty, the first actor language design supporting both static multiparty session typing and the full power of actors taking part in multiple sessions. Our main insight is to enforce session typing through a flow-sensitive type-and-effect system, combined with an event-driven programming style and first-class message handlers. Using MPSTs allows us to guarantee communication safety: a process will never send or receive an unexpected message, nor will it ever get stuck waiting for a message that will never arrive. We extend Maty to support both Erlang-style cascading failure handling and the ability to proactively switch between sessions. We implement Maty in Scala using an API generation approach, and evaluate our implementation on a series of microbenchmarks, a factory scenario, and a chat server.
2. Less is More Revisited (Nobuko Yoshida, Oxford)
   Multiparty session types (MPST) provide a type discipline where a programmer or architect specifies a whole view of communications as a global protocol, and each distributed program is locally type-checked against its end-point projection. After 10 years from the birth of MPST, Scalas and Yoshida discovered that the proofs of type safety in the literature which use the end-point projection with mergeability are flawed. After this paper, researchers wrongly believed that the end-point projection (with mergeability) was unsound. We correct this misunderstanding, proposing a new general proof technique for type soundness of multiparty session π-calculus, which uses an association relation between a global type and its end-point projection.
3. Session Subtyping by Fixpoint Acceleration (Andy King, Kent)
   We combine and apply three ancient techniques in the programming language literature (published thirty, fifty and sixty years ago) to the timely problem of session subtyping and conclude there is little new under the sun.
4. Non-linear communication via graded modal session types (Danielle Marshall, Glasgow)
   Session types provide guarantees about concurrent behaviour and can be understood through their correspondence with linear logic, with propositions as sessions and proofs as processes. However, strict linearity is limiting since there exist useful communication patterns that rely on non-linear behaviours. For example, shared channels can repeatedly spawn a process with binary communication along a fresh linear channel. Non-linearity can be introduced in a controlled way through the concept of graded modal types, which are a framework encompassing various kinds of coeffect (describing how computations make demands on their context). This paper shows how graded modalities can work alongside session types, enabling various non-linear concurrency behaviours to be re-introduced precisely. The ideas are demonstrated using Granule, a functional language with linear, indexed, and graded modal types. We define a core calculus capturing the requisite features and our new graded primitives, then present an operational model and establish various key properties.
5. Partial Probabilistic Multi Party Session Types (Joe Paulus, Oxford)
   Probabilistic concurrent programs are computational models that incorporate randomness to model uncertainties during execution. They are widely used to represent systems such as randomized algorithms, network protocols, and distributed systems. Probabilistic models help analyse performance metrics, reliability, and correctness under varying conditions. The importance of probabilistic concurrent programs lies in the ability to model and analyse systems that involve uncertainty and nondeterminism. These models are crucial for designing robust algorithms. Verification techniques for these systems ensure that they meet desired properties, such as safety, deadlock freedom, or specific probabilistic guarantees, making them crucial in scenarios where unpredictability plays a significant role.
6. Multiparty Session Types with a Bang! (Matthew Alan Le Brun, Glasgow)
   Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce MPST! a session-typed multiparty process calculus with replication and first-class roles. We find that replication is not an equivalent alternative to recursion in MPST, and using both replication and recursion in one type system in fact allows us to express both context-free protocols and protocols that make interesting use of mutual exclusion and races. We demonstrate the expressiveness of MPST! on examples including binary tree serialisation, the dining philosophers problem, and a model of an auction, and explore the implications of replication on the decidability of typechecking.
7. Mailboxer: Towards Early Detection of Erlang Communication Errors (Duncan Paul Attard, Malta)
   This talk introduces Mailboxer, a prototype tool for statically checking communication in Erlang codebases. Mailboxer enables developers to annotate processes with expected message types, allowing the tool to detect a wide range of communication errors at compile time. Early detection of such errors has the potential to significantly reduce debugging effort and development time. Existing session-type systems for Erlang and Elixir rely on channel-based communication approaches. By contrast, Mailboxer adopts a mailbox-typing discipline that aligns with the idiomatic message-passing style of Erlang actors. While the current prototype implementation targets Erlang, the underlying type theory and checking approach are applicable to other actor-based languages that employ mailboxes, such as Elixir and Scala/Akka.
8. Asynchronous Mixed Choices (A Unifying Framework for Failure Handling) (Laura Bocchi, Kent)