Compiling Multiparty Session Processes in Go

Supervisors

Functional Programming Languages and Concurrency

The GoPi project[1,2] aims at using an high level process language to automatically generated Go code that

at runtime (1) does not deadlock on channels declared as linear, and (2) does not enlarge the scope of

channels declared as static.

The GoPi compiler is a tool implemented in OCaml that relies on constraint solving to perform type inference of the

source-level processes, which do not contain type annotations. In particular, channels declared as linear

are assigned to linear types [3], and deadlock-freedom is obtained by inferring the order of usage of linear

channels.

The aim of this project is to study how to embed Multiparty Session Types[4,5] in GoPi.

This forthcoming feature will allow to describe more complex scenarios, and to generate code

with stronger properties.

Towards this direction, the student will study related work on Multiparty Session Types and type inference, and
describe how the existing methodologies and techniques could apply to the GoPi setting.
One of the applications of this study might be the development of constraints [6] that can be re-used in the
feature implementation.
The student will be in charge of finding a test suite of realistic examples of multiparty scenarios, and of
implementing the tests in Go. This will allow to study the behaviour of Go multiparty programs before the
deployment of the new release of GoPi.

[2] Giunti, M.: GoPi: Compiling linear and static channels in Go. COORDINATION 2020.

LNCS 12134, pp. 137–152. Springer (2020), https://doi.org/10.1007/978-3-030-50029-0_9

[3] Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus.

ACM Trans. Program. Lang. Syst. 21(5), 914–947 (1999), https:/doi.org/10.1145/330249.330251

[4] Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types.

POPL 2008. pp. 273–284. ACM (2008). https://doi.org/10.1145/1328438.1328472

[5] Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types.

J.ACM 63(1), 9:1–9:67 (2016). https://doi.org/10.1145/2827695

[6] Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report,

Department of Computer Science, The University of Iowa (2017)