Higher-order Context-free Session Types in System F

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.

In Marco Carbone and Rumyana Neykova: Proceedings of the 13th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2022), Munich, Germany, 3rd April 2022, Electronic Proceedings in Theoretical Computer Science 356, pp. 24–35.
Published: 24th March 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.356.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org