Diana Costa (LASIGE, Faculdade de Ciências, Universidade de Lisboa) |
Andreia Mordido (LASIGE, Faculdade de Ciências, Universidade de Lisboa) |
Diogo Poças (LASIGE, Faculdade de Ciências, Universidade de Lisboa) |
Vasco T. Vasconcelos (LASIGE, Faculdade de Ciências, Universidade de Lisboa) |
We present an extension of System F with higher-order context-free session types. The mixture of functional types with session types has proven to be a challenge for type equivalence formalization: whereas functional type equivalence is often rule-based, session type equivalence usually follows a semantic approach based on bisimulations. We propose a unifying approach that handles the equivalence of functional and session types together. We present three notions of type equivalence: a syntactic rule-based version, a semantic bisimulation-based version, and an algorithmic version by reduction to the problem of bisimulation of simple grammars. We prove that the three notions coincide and derive a decidability result for the type equivalence problem of higher-order context-free session types. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.356.3 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |