π-calculus, Session Types research at Imperial College

Fluid Session Types: End-to-End Verification of Communication Protocols
April 2019 - March 2023

The primary objective of this PhD project, funded by VeTSS, is the verification of distributed protocols using session types.

This grant is associated to the PhD studentship of Nicolas, who works on the implementation of Multiparty Session Types in Rust. This work aims for the development of theory and tools to automate the creation and verification of distributed protocols in Rust, including checking for different kinds of errors through safety properties, ensuring channel liveness, and other extensions including the formalisation of MPST for affine channels.
Related publications