Supervisors

Suitable for

Abstract

Prerequisites:  Concurrency, concurrent programming and functional programming. It is ideal if the student took Lambda Calculus and Types

 

Background

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.

 

Focus

The aim of this project is to embed Multiparty Session Types [4,5] in GoPi, thus allowing to describe

more complex scenarios, and to generate code with stronger properties.

 

Method

Towards this direction, the student will study related work on Multiparty Session Types and type inference, and

apply the existing methodologies and techniques to the GoPi setting.

This will involve the development of automatically generated constraints[6] to implement the type inference procedure.

 

The student will attack the problem of deploying techniques to assign Multiparty Session Types to processes,

and of implementing it in GoPi. The final objective is to automatically generate deadlock-free Go code

that implements well-typed multiparty processes, and to assess to the validity of the implementation by identifying

a test suite of realistic multiparty scenarios.

 

References

[1] Giunti, M.: The GoPi compiler (June 2019), https://sites.fct.unl.pt/gopi/, Git: https://github.com/marcogiunti/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)