On the Mechanisation of Multiparty Asynchronous Session Types

Marco Carbone ( ITU Copenhagen )

Multiparty session types is a typing discipline used for writing protocol specifications, known as global types, for branching and recursive message-passing systems. MECHANIST is a research project whose aim is to mechanise the full theory of multiparty session types.  In this talk, I will give an overview of the outcome of the project and, in particular, I will focus on two key results: the definition of a new projection function, a necessary operation on global types for abstracting local behaviour to connect to process code; and, the proof of the main theorem from the original theory, namely subject reduction (which ensures typability is preserved through reductions). All results have been mechanised in the Coq proof assistant. 

This is a joint work with Dawit Tirore and Jesper Bengtson. The results on projection appeared in the proceedings of ITP’23.