Session Type Isomorphisms
Mariangiola Dezani-Ciancaglini (Universita' di Torino), Luca Padovani, (Universita' di Torino), Jovanka Pantovic (Univerzitet u Novom Sadu)

TL;DR
This paper explores the concept of session type isomorphisms, providing semantic and axiomatic characterizations, and discusses the complexity and open problems related to their axiomatization.
Contribution
It introduces a formal theory of session type isomorphisms, highlighting their semantic properties and the challenges in axiomatization and completeness.
Findings
Semantic characterization of session type isomorphisms
Identification of non-finite axiomatizability issues
Discussion of open problems in axiomatization and completeness
Abstract
There has been a considerable amount of work on retrieving functions in function libraries using their type as search key. The availability of rich component specifications, in the form of behavioral types, enables similar queries where one can search a component library using the behavioral type of a component as the search key. Just like for function libraries, however, component libraries will contain components whose type differs from the searched one in the order of messages or in the position of the branching points. Thus, it makes sense to also look for those components whose type is different from, but isomorphic to, the searched one. In this article we give semantic and axiomatic characterizations of isomorphic session types. The theory of session type isomorphisms turns out to be subtle. In part this is due to the fact that it relies on a non-standard notion of equivalence…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
