On the relative expressiveness of higher-order session processes

Dimitrios Kouzapas; Jorge A. Perez; Nobuko Yoshida

doi:10.1016/j.ic.2019.06.002

On the relative expressiveness of higher-order session processes

Dimitrios Kouzapas^*, Jorge A. Perez, Nobuko Yoshida

^*Corresponding author for this work

Fundamental Computing

Research output: Contribution to journal › Article › Academic › peer-review

7 Citations (Scopus)

21 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 language	English
Article number	104433
Number of pages	54
Journal	Information and Computation
Volume	268
DOIs	https://doi.org/10.1016/j.ic.2019.06.002
Publication status	Published - Oct-2019

Keywords

Concurrency
Process calculi
Behavioural types
Session types
Expressiveness
LINEARITY
CALCULUS

Access to Document

10.1016/j.ic.2019.06.002

Final aut- On the relative expressiveness of higher-order session processesFinal author's version, 617 KBLicence: CC BY-NC-ND

Handle.net

Persistent link

Embargoed Document

On the relative expressiveness of higher-order session processes
Final publisher's version, 1.2 MB
Request copy

1 Academic presentation

Session Types and Higher-Order Concurrency
Jorge Perez Parra (Invited speaker)
24-Feb-2021
Activity: Talk and presentation › Academic presentation › Academic

Cite this

@article{44b8ef9f859a4753b6dcc5c3ca32e67d,

title = "On the relative expressiveness of higher-order session processes",

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.",

keywords = "Concurrency, Process calculi, Behavioural types, Session types, Expressiveness, LINEARITY, CALCULUS",

author = "Dimitrios Kouzapas and Perez, {Jorge A.} and Nobuko Yoshida",

year = "2019",

month = oct,

doi = "10.1016/j.ic.2019.06.002",

language = "English",

volume = "268",

journal = "Information and Computation",

issn = "0890-5401",

publisher = "ACADEMIC PRESS INC ELSEVIER SCIENCE",

}

TY - JOUR

T1 - On the relative expressiveness of higher-order session processes

AU - Kouzapas, Dimitrios

AU - Perez, Jorge A.

AU - Yoshida, Nobuko

PY - 2019/10

Y1 - 2019/10

N2 - 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.

AB - 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.

KW - Concurrency

KW - Process calculi

KW - Behavioural types

KW - Session types

KW - Expressiveness

KW - LINEARITY

KW - CALCULUS

U2 - 10.1016/j.ic.2019.06.002

DO - 10.1016/j.ic.2019.06.002

M3 - Article

VL - 268

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

M1 - 104433

ER -

On the relative expressiveness of higher-order session processes

Abstract

Keywords

Access to Document

Handle.net

Embargoed Document

Activities

Session Types and Higher-Order Concurrency

Cite this