π-calculus, Session Types research at Imperial College

A Gentle Adventure Mechanising Message Passing Concurrency Systems

Tutorial at VEST'21.

We discuss three aspects of mechanising binary and multiparty session types in the Coq proof assistant. We talk about mechanising binary session types with a locally nameless binder representation (a deep embedding of binders), the design of Zooid a multiparty process language that favours shallow embeddings of binders, and finally, our mechanisation of trace equivalence for global, and local types, and with Zooid process traces. This is presented as a tutorial designed from simplified versions of our mechanisation of binary and multiparty session types that are both more accessible and provide exercises.