Higher-Order Processes, Functions, and Sessions: A Monadic Integration
Higher-Order Processes, Functions, and Sessions: A Monadic Integration
复制标题
高阶流程、函数和会话：单子集成
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
F. Pfenning
中科院分区：
文献类型：
--
作者：
Bernardo Toninho;Luís Caires;F. Pfenning
在以前的研究中，我们已经开发了一个Curry-Howard解释的线性微积分会话类型的过程。在本文中，我们统一集成这种计算解释的函数语言通过一个线性上下文单子，隔离基于会话的并发。一元值是开放的进程表达式，是语言中的第一类对象，因此为高阶会话类型进程提供了逻辑基础。我们说明了如何结合使用的单子和递归类型，使我们能够干净地编写各种并发程序，包括高阶程序的通信进程。我们展示了类型保持的标准元理论结果，以及一个全局进展定理，据我们所知，这在高阶会话类型设置中是新的。
In prior research we have developed a Curry-Howard interpretation of linear sequent calculus as session-typed processes. In this paper we uniformly integrate this computational interpretation in a functional language via a linear contextual monad that isolates session-based concurrency. Monadic values are open process expressions and are first class objects in the language, thus providing a logical foundation for higher-order session typed processes. We illustrate how the combined use of the monad and recursive types allows us to cleanly write a rich variety of concurrent programs, including higher-order programs that communicate processes. We show the standard metatheoretic result of type preservation, as well as a global progress theorem, which to the best of our knowledge, is new in the higher-order session typed setting.