A Sound and Complete Projection for Global Types

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review


Multiparty session types is a typing discipline used to write specifications, known as global types, for branching and recursive message-passing systems. A necessary operation on global types is projection to abstractions of local behaviour, called local types. Typically, this is a computable partial function that given a global type and a role erases all details irrelevant to this role.
Computable projection functions in the literature are either unsound or too restrictive when dealing with recursion and branching. Recent work has taken a more general approach to projection defining it as a coinductive, but not computable, relation. Our work defines a new computable projection function that is sound and complete with respect to its coinductive counterpart and, hence, equally expressive. All results have been mechanised in the Coq proof assistant.
Original languageEnglish
JournalLeibniz International Proceedings in Informatics
Pages (from-to)28:1
Number of pages28
Publication statusPublished - 26 Jul 2023


  • Session types
  • Mechanisation
  • Projection
  • Coq


Dive into the research topics of 'A Sound and Complete Projection for Global Types'. Together they form a unique fingerprint.

Cite this