MobilityReadingGroup

On the Relative Expressiveness of Higher-Order Session Processes

Dimitrios KOUZAPAS , Jorge A. PÉREZ , Nobuko YOSHIDA

By integrating constructs from the λ-calculus and the π-calculus, in higher-order process calculi exchanged values may contain processes.This paper studies the relative expressiveness of HOπ, the higher-order π-calculus in which communications are governed by session types. Our main discovery is that HO,a subcalculus of HOπ which lacks name-passing and recursion, can serve as a new core calculus for session-typed higher-order concurrency. By exploring a new bisimulation for HO, we show that HO can encode HOπ fully abstractly (up to typed contextual equivalence) more precisely and efficiently than the first-order session π-calculus (π). Overall, under session types, HOπ, HO, and π are equally expressive; however, HOπ and HO are more tightly related than HOπ and π.

@inproceedings{KPY2016,
  author = {Dimitrios Kouzapas and Jorge A. Pérez and Nobuko Yoshida},
  title = {{On the Relative Expressiveness of Higher-Order Session Processes}},
  booktitle = {25th European Symposium on Programming},
  series = {LNCS},
  volume = {9632},
  pages = {446--475},
  publisher = {Springer},
  year = 2016
}

@inproceedings{KPY2016,
  author = {Dimitrios Kouzapas and Jorge A. Pérez and Nobuko Yoshida},
  title = {{On the Relative Expressiveness of Higher-Order Session Processes}},
  booktitle = {25th European Symposium on Programming},
  series = {LNCS},
  volume = {9632},
  pages = {446--475},
  publisher = {Springer},
  doi = "10.1007/978-3-662-49498-1_18",
  year = 2016
}