论文标题
系统f中的高阶无上下文会话类型
Higher-order Context-free Session Types in System F
论文作者
论文摘要
我们提出了具有高阶无上下文会话类型的系统F的扩展。事实证明，功能类型与会话类型的混合物是类型等效形式化的挑战：虽然功能类型等效性通常是基于规则的，但会话类型等效性通常遵循基于双击的语义方法。我们提出了一种统一的方法，可以一起处理功能和会话类型的等效性。我们提出了类型等效的三个概念：基于句法规则的版本，基于语义分配的版本，以及通过简单仿真简单语法的问题来示例版本。我们证明，这三个概念重合并得出了高阶无上下文会话类型类型等效问题的确定性结果。
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.
