Mailbox Actors

4. Metatheoretic Properties🔗

Five metatheoretic properties are established for the mailbox actor system (Section 5 of the paper). All proofs are fully machine-checked with zero uses of sorry or admit.

  1. 4.1. Type Preservation (Proposition 1)
  2. 4.2. Progress (Proposition 2)
  3. 4.3. Effect Determinism (Proposition 3)
  4. 4.4. Mailbox Isolation (Proposition 4)
  5. 4.5. Eventual Delivery (Proposition 5)