[DPP+14] Session Type Isomorphisms

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 between processes. In addition, we do not know whether the axiomatization is complete. It is known that the isomorphisms for arrow, product and sum types are not finitely axiomatisable, but it is not clear yet whether this negative results holds also for the family of types we consider in this work.

@inproceedings{DezaniPadovaniPantovic14, volume = {155}, author = {Mariangiola Dezani-Ciancaglini and Luca Padovani and Jovanka Pantovic}, series = {EPTCS}, booktitle = {Proceedings of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES'14)}, url = {http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?PLACES2014.9.pdf}, 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 between processes. In addition, we do not know whether the axiomatization is complete. It is known that the isomorphisms for arrow, product and sum types are not finitely axiomatisable, but it is not clear yet whether this negative results holds also for the family of types we consider in this work. }, title = {{Session Type Isomorphisms}}, publisher = {Open Publishing Association}, year = {2014}, pages = {61-71}, doi = {10.4204/EPTCS.155.9}, }

DezaniPadovaniPantovic14 (In proceedings)
Author(s)	Mariangiola Dezani-Ciancaglini, Luca Padovani and Jovanka Pantovic
Title	« Session Type Isomorphisms »
In	Proceedings of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES'14)
Series	EPTCS
Volume	155
Page(s)	61-71
Year	2014
Publisher	Open Publishing Association
URL	http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?PLACES2014.9.pdf