Mailbox Types for Unordered Interactions
We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks in the mailbox calculus, a mild extension of the asynchronous π-calculus with first-class mailboxes and selective input. The calculus subsumes the actor model and allows us to analyze networks with dynamic topologies and varying number of processes possibly mixing different concurrency abstractions. Well-typed processes are deadlock free and never fail because of unexpected messages. For a non-trivial class of them, junk freedom is also guaranteed. We illustrate the expressiveness of the calculus and of the type system by encoding instances of non-uniform, concurrent objects, binary sessions extended with joins and forks, and some known actor benchmarks.
Fri 20 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
| 11:00 - 12:40 | |||
| 11:0025m Research paper | KafKa: Gradual Typing for Objects ECOOP Research Papers Benjamin Chung Northeastern University, Paley Li Northeastern University, Francesco Zappa Nardelli Inria, Jan Vitek Northeastern UniversityDOI | ||
| 11:2525m Research paper | Dependent Types for Class-based Mutable Objects ECOOP Research PapersDOI | ||
| 11:5025m Research paper | Static typing of complex presence constraints in interfaces ECOOP Research Papers Nathalie Oostvogels Vrije Universiteit Brussel, Joeri De Koster Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit BrusselDOI | ||
| 12:1525m Research paper | Mailbox Types for Unordered Interactions ECOOP Research PapersDOI | ||
