Linear logical relations and observational equivalences for session-based concurrency
Linear logical relations and observational equivalences for session-based concurrency
复制标题
基于会话的并发的线性逻辑关系和观察等价
DOI：
10.1016/j.ic.2014.08.001
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Bernardo Toninho
中科院分区：
文献类型：
--
作者：
Jorge A. Pérez;Luís Caires;F. Pfenning;Bernardo Toninho
在基于会话的并发领域，我们研究了强规范性、汇聚性和行为等价性。这些相互关联的问题为结构化通信模型中的高级正确性分析奠定了基础。我们研究的起点是将线性逻辑命题解释为交流过程的会话类型，这是以前的工作中提出的。强大的规范性和汇合性是通过发展逻辑关系理论来建立的。定义在线性类型结构上，我们的逻辑关系仍然与函数式语言的逻辑关系非常相似。我们还为会话类型的过程引入了观察等价的自然概念。作为应用，我们证明了由逻辑解释产生的所有证明转换实际上都表示观察等价，并解释了由线性逻辑等价产生的类型同构是如何通过基于会话的并发系统的接口类型之间的强制来实现的。
We investigatestrong normalization,confluence, andbehavioral equalityin the realm of session-based concurrency. These interrelated issues underpin advanced correctness analysis in models of structured communications. The starting point for our study is an interpretation of linear logic propositions as session types for communicating processes, proposed in prior work. Strong normalization and confluence are established by developing a theory oflogical relations. Defined upon a linear type structure, our logical relations remain remarkably similar to those for functional languages. We also introduce a natural notion ofobservational equivalencefor session-typed processes. Strong normalization and confluence come in handy in the associated coinductive reasoning: as applications, we prove that allproof conversionsinduced by the logic interpretation actually express observational equivalences, and explain howtype isomorphismsresulting from linear logic equivalences are realized by coercions between interface types of session-based concurrent systems.