2022/03/23 by Diana Costa, Andreia Mordido, Diogo Poças +1 · 1 citation
Computer Science · Mathematics · #Artificial intelligence #Bisimulation #Computer science #Context (archaeology) #Decidability #Discrete mathematics #Equivalence (formal languages) #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Logical equivalence #Mathematics #Rule-based machine translation #Session (web analytics) #Theoretical computer science #Type (biology) #Type theory #cs.FL #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.356.3
published as EPTCS 356, 2022, pp. 24-35 · In Proceedings PLACES 2022, arXiv:2203.12142
openalex publication_date 2022/03/23 · arxiv created 2022/03/24 · arxiv updated 2022/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.