MobilityReadingGroup

Service Equivalence via Multiparty Session Type Isomorphisms

Assel ALTAYEVA, Nobuko YOSHIDA

Concurrent and distributed programming is notoriously hard. Modern languages and toolkits address the challenge by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g., Go): they allow for simpler reasoning w.r.t. shared-memory concurrency, but do not ensure that a program implements a given specification. To address this challenge, it would be desirable to specify and verify the intended behaviour of message-passing applications using types, and ensure that, if a program type-checks and compiles, then it will run and communicate as desired. We develop this idea in theory and practice. We formalise a concurrent functional language $\lambda^{\pi}_{\leq}$, with a new blend of behavioural types (from $\pi$-calculus theory), and dependent function types (from the Dotty programming language, a.k.a. the future Scala 3). This theory yields four main payoffs: (1) it verifies safety and liveness properties of programs via type– level model checking; (2) unlike previous work, it accurately verifies channel-passing (covering a typical pattern of actor programs) and higher-order interaction (i.e., sending/receiving mobile code); (3) it is directly embedded in Dotty, as a toolkit called Effpi, offering a simplified actor-based API; (4) it enables an efficient runtime system for Effpi, for highly concurrent programs with millions of processes/actors.

@inproceedings{AY2019,
  author = {Assel Altayeva and Nobuko Yoshida},
  title = {{Service Equivalence via Multiparty Session Type Isomorphisms}},
  booktitle = {Proceedings Programming Language Approaches to Concurrency and Communication-cEntric Software},
  volume = {291},
  pages = {1--11},
  publisher = {Open Publishing Association},
  year = 2019
}

@inproceedings{AY2019,
  author = {Assel Altayeva and Nobuko Yoshida},
  title = {{Service Equivalence via Multiparty Session Type Isomorphisms}},
  booktitle = {Proceedings Programming Language Approaches to Concurrency and Communication-cEntric Software},
  volume = {291},
  pages = {1--11},
  publisher = {Open Publishing Association},
  doi = "10.4204/EPTCS.291.1",
  year = 2019
}