Computer Sciences Colloquium - Dr. Sung-Shik Jongmans, University of Groningen

Title: Recent advances in multiparty session typing

Abstract:

*Multiparty session typing* (MPST) is a method to make concurrent programming simpler. The idea is to use type checking to automatically prove *safety* (compliance) and *liveness* (communication deadlock freedom) of protocol implementations relative to specifications. In this talk, I'll present a few recent advances in MPST research:

1. In the first part (based on a paper in TACAS'25), I'll introduce MPST practice in the form of a new Scala library for MPST-based programming, called `mpst.embedded`. Essentially, `mpst.embedded` is an *internal* domain-specific language to specify protocols, embedded in Scala. To assure safety and liveness, the library takes advantage of Scala's lightweight form of dependent types, called *match types*.

2. In the second part (based on a paper in ECOOP'23), I'll introduce MPST theory in the form of a new approach to MPST-based program analysis. The main difference is that typing rules are *analytic* in existing approaches, while they are *synthetic* in this new approach. An advantage is improved expressiveness: fewer safe/live protocol implementations are conservatively rejected using the synthetic approach than in the analytic approach.