Duncan Paul Attard is a postdoctoral researcher at the University of Glasgow in the UK. He has a PhD in Computer Science from Reykjavik University (Iceland) and the University of Malta (Malta). His main research interests lie in runtime monitoring and verification for concurrent systems, the automated synthesis of efficient runtime monitors, and software engineering techniques to address scalability and partial failure in distributed systems. He is also interested in the semantics of programming languages, language design, and concurrent languages. Duncan works at the University of Glasgow on safe communication in concurrent languages using Mailbox Types.
The talk presents and demonstrates a new prototype communication checking tool for Erlang codebases: Mailboxer.
If a developer annotates parts of an Erlang codebase with expected message types Mailboxer can statically detect many communication errors in the annotated processes. So errors like unreceived messages, some deadlocks, protocol violations, typos in message tags etc. Finding errors early in development reduces debugging and development times.
Existing session type checkers for Erlang and Elixir enforce channel, rather than mailbox, based communication. In contrast Mailbox types check communication using idiomatic mailbox communication. Currently Mailboxer targets Erlang, but the type theory and checking technology apply to other actor languages with mailboxes, so Elixir, Scala/Akka and others.
Erlang will be the first production language to benefit from a radically new communication checking tool.
Key Takeaways:
Target Audience: