A Sound and Complete Projection for Global Types

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer 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.
TidsskriftLeibniz International Proceedings in Informatics
Sider (fra-til)28:1
Antal sider28
StatusUdgivet - 26 jul. 2023


Dyk ned i forskningsemnerne om 'A Sound and Complete Projection for Global Types'. Sammen danner de et unikt fingeraftryk.