ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Mon 4 Sep 2023 15:15 - 15:30 at Adams - Erlang Workshop: Session 2 Chair(s): Kiko Fernandez-Reyes

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.

Mon 4 Sep

Displayed time zone: Pacific Time (US & Canada) change

14:00 - 15:30
Erlang Workshop: Session 2Erlang at Adams
Chair(s): Kiko Fernandez-Reyes Ericsson, Sweden
Invited Talk: Set-theoretic Types for Erlang
Albert Schimpf University of Kaiserslautern-Landau, Stefan Wehr Offenburg University of Applied Sciences, Annette Bieniusa University of Kaiserslautern-Landau
Link to publication DOI Authorizer link Pre-print
Mria: an eventually consistent MnesiaRemote
Dmitrii Fedoseev , Serhii Tupchii EMQ Technologies, Thales Macedo Garitezi EMQ Technologies, Zaiming Shi EMQ Technologies
Lightning Talk: Towards Mailbox Typing for Erlang
Simon Fowler University of Glasgow