Mailbox Actors
This is the machine-checked companion to the paper Mailbox Actors (submitted, under revision).
We present a formal framework for actor systems in which mailboxes are promoted to independent, first-class actors — native actors with their own configuration, behaviour, and lifecycle. Each processing actor is automatically paired with a dedicated mailbox actor whose guarded-action behaviour governs delivery, filtering, and scheduling, enabling modular mailbox implementations while adding no burden for simple engines that need only the default first-in-first-out policy.
Every definition, proposition, and example below is type-checked by the
Lean 4 theorem prover. There are zero uses of
sorry or admit in the formalization.
Citation
J. Prieto-Cubides, A. Hart, T. Heindel. Mailbox Actors. 2025.