Lightning Talk: Towards Mailbox Typing for Erlang
summary
Mailbox types assign a state to a process mailbox as a commutative regular expression to statically detect protocol violations, payload mismatches, and self-deadlocks (example: an ID server must see exactly one init and many get messages; mistakes include forgotten replies, duplicate init, self-deadlock, or misspelled tags). Work produces a core-calculus theory plus an OCaml typechecker that generates regex-inclusion constraints solved with Z3, and proposes an Erlang frontend with lightweight annotations that scope mailboxes per function to keep analysis scalable.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:01Example
- 2:02Troubleshooting
- 4:05Tools
- 5:15Mailbox Types
- 7:01Mailbox Life Cycle
- 7:50Mailbox Typing for Erlang
- 9:39Annotations
- 12:34Questions
related talks
26mSpecial Delivery: Programming with Mailbox Types
12mObject Oriented Thinking with Elixir and OTP
39mProtocol engineering for communicating actors
40mTypes and Erlang from Dialyzer to (...)
51mThe Erlang VM or How I Started Loving Parallel Progamming
20mMessage-Observing Sessions
01h 01mThe Erlang Ecosystem
39mConcurrency Oriented Programming In A Modern World