π-calculus, Session Types research at Imperial College
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.
Organisers
Links