We are interested in the rigorous verification of message-passing programs, which operate by exchanging messages across distributed networks. Ensuring that these communicating programs are correct is important but highly challenging.

Originated from the realms of Concurrency Theory and Programming Languages, Multiparty Session Types (MPSTs) offer a convenient methodology for the development and verification of message-passing programs. The methodology of MPSTs offers a structured approach to the design of advanced verification techniques, both static (via type systems) and dynamic (via monitoring architectures). Interestingly, these static and verification techniques can be defined by following principled approaches based on resource-aware logics, in particular Girard’s Linear Logic.

In this talk, I will overview recent work by my group in this direction and highlight a number of open challenges and opportunities.

I am an associate professor at the University of Groningen (The Netherlands), where I lead the research group Fundamental Computing.