Although actor-based languages like Erlang and Elixir eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to concurrency errors such as protocol violations and deadlocks. Mailbox types are a very new technique, complementary to existing tools like the Concuerror model checker, that allow us to detect concurrency errors.

Mailbox types characterise the state of a processes mailbox using a commutative regular expression, and can rule out protocol violations, payload mismatches, and self-deadlocks.

At ICFP’23, we show how mailbox types can statically detect concurrency errors in a core actor-based programming language. This short talk will introduce mailbox typing and describe our ongoing work developing a mailbox typing tool for detecting concurrency errors in Erlang codebases.

This is joint work with Duncan Paul Attard, Simon J. Gay, and Phil Trinder, and is part of the STARDUST project https://epsrc-stardust.github.io/

I’m a Lecturer in Programming Language Foundations at the University of Glasgow School of Computing Science.

My research interests centre around typed functional programming languages, in particular functional approaches to concurrency, web programming, and data management.

Previously, I worked on the STARDUST project, investigating behavioural types for actor systems, working with Simon Gay and Phil Trinder. Before that, I spent 6 years at the University of Edinburgh School of Informatics, first as a PhD student in the Centre for Doctoral Training in Pervasive Parallelism working with Sam Lindley and Philip Wadler, and second as a Research Software Engineer working with James Cheney. I’ve also worked at OCaml Labs and IntelliFactory.