Supervisors

Suitable for

Abstract

Prerequisites: None

Background

Asynchronous Multiparty Session Types (MPST) provide a formal framework for specifying and verifying communication protocols in distributed systems that use asynchronous message passing. Unlike synchronous MPST, where communication is blocked until a message is received, the asynchronous model allows messages to be sent and buffered without requiring immediate receipt. Subtyping in asynchronous MPST facilitates optimised programs while maintaining type safety and deadlock freedom. This optimisation is achieved through message reordering, which allows messages to be sent earlier or received later. As a result, a process implementing type T can safely replace one implementing type T', as long as T is a subtype of T'.

Focus

The goal of this project is to prove several examples of asynchronous subtyping in Coq and establish basic metaproperties such as transitivity and antisymmetry, building on the existing formalisation [1].

Method

Since subtyping is defined coinductively, proving these properties requires coinductive reasoning in Coq. To achieve this we employ the parametrissed coinduction technique [2], implemented by the Paco library [3].

[1] Burak Ekici and Nobuko Yoshida. "Completeness of Asynchronous Session Tree Subtyping in Coq," ITP 2024.

[2] Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. "The Power of Parameterization in Coinductive Proof," POPL 2013.

[3] https://github.com/snu-sf/paco