Higher-order Context-free Session Types in System F

Autor:	Costa, Diana, Mordido, Andreia, Poças, Diogo, Vasconcelos, Vasco T.
Rok vydání:	2022
Předmět:	Computer Science - Logic in Computer Science Computer Science - Formal Languages and Automata Theory Computer Science - Programming Languages
Zdroj:	EPTCS 356, 2022, pp. 24-35
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.356.3
Popis:	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. Comment: In Proceedings PLACES 2022, arXiv:2203.12142
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2203.12877 Zobrazit plný text záznamu View this record from Arxiv