Concurrent programming, session types, and proof assistants

8^th December 2023, 14:00
Lorenzo Gheri

Abstract

Formally and correctly reasoning about programs and their behaviour is a challenging and error-prone task. In the case of concurrency, (multiparty) session types have stood the test of time as a specification and verification framework for distributed message-passing systems. However, on the one hand, pen-on-paper proofs have carried limitations and mistakes, thus calling for the mechanised help of proof assistants. On the other hand, the growing scale and the constant evolution of real-world distributed systems call for added flexibility and modularity in session-type specification and verification.

In this talk, I will introduce my research on the two non-disjoint topics of proof assistants and session types, for the specification and verification of concurrent programming. I will present some results and discuss future directions.