Supervisors

Suitable for

Abstract

Prerequisites: 

Concurrency and Functional Programming

 

Background

Session types are an effective method to control the behaviour of software components

that run in distributed systems communicating through message passing [1,2].

Multiparty session types [3,4] provide support for sessions involving multiple participants,

thus allowing to represent more expressive scenarios.

 

Focus

In this project, we are interested in calculating properties of multiparty session

types by using automated deductive verification performed in tools of the OCaml

ecosystem relying on Why3 [5,6].

In particular, we are interested in studying functions that compute the behaviour of

session type environments, and in verifying these functions automatically, when possible,

and interactively when the proof goals require transformations.

 

Method

Towards this direction, the student will study related work on multiparty session types

and automated deductive verification, and describe how the existing methodologies and

techniques could apply to the project's setting.

The student will be in charge of finding a test suite of realistic examples of multiparty

scenarios, and of implementing the tests in Why3. This will allow to study the behaviour

of multiparty session types in Why3 before the deployment of the verification proofs.

 

References

[1] Honda, K.: Types for dyadic interaction. CONCUR 1993.

LNCS 715, pp. 509–523. Springer (1993), https://doi.org/10.1007/3-540-57208-2_35

[2] Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline

for structured communication-based programming. ESOP 1998.

LNCS 1381, pp. 122–138. Springer (1998). https://doi.org/10.1007/BFb0053567

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

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

[4] 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

[5] Filliâtre, J., Paskevich, A.: Why3 - where programs meet provers.

ESOP 2013, LNCS 7792, pp. 125–128. Springer (2013).

https://doi.org/10.1007/978-3-642-37036-6_8

[6] Bobot, F., Filliâtre, J., Marché, C., Melquiond, G., Paskevich, A.:

The Why3 Platform. Version: 1.7, April 2024. https://www.why3.org/doc/index.html