Supervisor

Suitable for

Abstract

Multiparty session types (MPST) offer a specification and verification framework for concurrency: communicating systems can be safely implemented in a distributed fashion, when well-typed against local session types, provided that such local types are obtained by projection of a single choreographic protocol (global type).

Multiple projects are available, please get in touch with nobuko.yoshida@cs.ox.ac.uk for more detail.

Possible aims are: (i) exploring and implementing an algorithms for MPST protocol compositionality or (ii) formalising correctness of advanced MPST systems (e.g., featuring merge, subtyping, or delegation). Students with a strong interest in the mechanisation of MPST in proof assistants (Coq, Isabelle, Idris) are very welcome to reach out.

[1] Mechanisation Paper https://dl.acm.org/doi/10.1145/3453483.3454041

[2] Multiparty Session Types Paper https://link.springer.com/chapter/10.1007/978-3-030-36987-3_5