MobilityReadingGroup

Nested Protocols in Session Types

Romain DEMANGEON, Kohei HONDA

We propose an improvement to session-types, introducing nested protocols, the possibility to call a subprotocol from a parent protocol. This feature adds expressiveness and modularity to the existing session-type theory, allowing arguments to be passed and enabling higher-order protocols definition. Our theory is introduced through a new type system for protocols handling subprotocol calls, and its implementation in a session-calculus. We propose validation and satisfaction relations between specification and implementation. Sound behaviour is enforced thanks to the usage of kinds and well-formedness, allowing us to ensure progress and subject reduction. In addition, we describe an extension of our framework allowing subprotocols to send back results.

@inproceedings{DH2012,
  author = {Romain Demangeon and Kohei Honda},
  title = {{Nested Protocols in Session Types}},
  booktitle = {23rd International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {7454},
  pages = {272--286},
  publisher = {Springer},
  year = 2012
}

@inproceedings{DH2012,
  author = {Romain Demangeon and Kohei Honda},
  title = {{Nested Protocols in Session Types}},
  booktitle = {23rd International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {7454},
  pages = {272--286},
  publisher = {Springer},
  doi = "10.1007/978-3-642-32940-1_20",
  year = 2012
}