2026-07-19T21:12:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18403 2024-03-06T11:01:48Z ddc:004 open_access

A Sound and Complete Projection for Global Types Tirore, Dawit Bengtson, Jesper Carbone, Marco Session types Mechanisation Projection Coq 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dawit Tirore and Jesper Bengtson and Marco Carbone 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.28 urn:nbn:de:0030-drops-184039 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.28 eng https://creativecommons.org/licenses/by/4.0/legalcode