Supervisors

Suitable for

Abstract

Prerequisites:  Concurrency, concurrent programming and functional programming, Lambda Calculus and Types

 

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 apply the existing methodologies and

techniques to the project's setting.

 

The student will attack the problem of implementing the computable functions in tools

of the OCaml ecosystem, and of empirically evaluating their behaviour by

identifying a test suite of realistic examples of multiparty scenarios.

The final goal is to perform the verification of the functions in the Why3 platform,

which will eventually rely on both automated constraint solving and proof interaction.

 

 

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