Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

deLiguoroP18 (In proceedings)
Author(s) Ugo de' Liguoro and Luca Padovani
Title« Mailbox Types for Unordered Interactions »
In32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands
Page(s)15:1--15:28
Year2018
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik
URLhttps://doi.org/10.4230/LIPIcs.ECOOP.2018.15
Abstract
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 pi-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.

BibTeX code

@inproceedings{deLiguoroP18,
  author = {Ugo de' Liguoro and Luca Padovani},
  booktitle = {32nd European Conference on Object-Oriented Programming, {ECOOP}
               2018, July 16-21, 2018, Amsterdam, The Netherlands},
  url = {https://doi.org/10.4230/LIPIcs.ECOOP.2018.15},
  tag = {ECOOP 2018},
  title = {Mailbox Types for Unordered Interactions},
  abstract = {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 pi-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. },
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year = {2018},
  doi = {10.4230/LIPIcs.ECOOP.2018.15},
  pages = {15:1--15:28},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!