On the relative expressiveness of higher-order session processes

Dimitrios Kouzapas*, Jorge A. Perez, Nobuko Yoshida

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
2 Downloads (Pure)

Abstract

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

Original languageEnglish
Article number104433
Number of pages54
JournalInformation and Computation
Volume268
DOIs
Publication statusPublished - Oct-2019

Keywords

  • Concurrency
  • Process calculi
  • Behavioural types
  • Session types
  • Expressiveness
  • LINEARITY
  • CALCULUS

Cite this