Mailbox Actors

Formal framework for actor systems in which mailboxes are promoted to independent, first-class actors with their own configuration, behaviour, and lifecycle. Formalised in predicative Martin-Lof type theory.

• Paper: main.pdf (LaTeX, XeTeX)
• Lean 4 formalization: formalization/MailboxActors/
• Online spec: jonaprieto.github.io/mailbox-actors (Verso, type-checked by Lean)

Citing

The paper has been submitted and is currently under revision. The latest PDF is available in this repository: main.pdf.

@misc{prieto2025mailboxactors,
  title        = {Mailbox Actors},
  author       = {Jonathan Prieto-Cubides and Anthony Hart and Tobias Heindel},
  year         = {2025},
  note         = {Submitted, under revision},
  doi          = {10.5281/zenodo.14915469},
  url          = {https://doi.org/10.5281/zenodo.14915469}
}

Building the paper

Requires LaTeXMk and XeTeX:

make

See the Makefile for alternative engines (lualatex, pdflatex).

Building the formalization

Requires Lean 4 (see lean-toolchain for the exact version):

cd formalization/MailboxActors
lake build

Building the online spec

cd formalization/MailboxActors
lake build generate-spec
lake exe generate-spec

The generated site will be in formalization/MailboxActors/_out/html-multi/.