论文标题
高阶递归过程的域语义
A Domain Semantics for Higher-Order Recursive Processes
论文作者
论文摘要
两极分化的窗台编程语言统一地整合了功能编程和会话类型的消息串联并发。它支持一般递归，异步和同步通信以及传达渠道和流程的高阶程序。我们给两极分化的基林作为域理论语义 - - 具有这种功能组合的语言的第一个语义语义。两极分化的窗台中的会话类型表示单向通信的域。过程表示这些域之间的连续函数，过程组成由痕量操作员解释。我们通过验证预期的程序等价来说明我们的语义。
The polarized SILL programming language uniformly integrates functional programming and session-typed message-passing concurrency. It supports general recursion, asynchronous and synchronous communication, and higher-order programs that communicate channels and processes. We give polarized SILL a domain-theoretic semantics---the first denotational semantics for a language with this combination of features. Session types in polarized SILL denote pairs of domains of unidirectional communications. Processes denote continuous functions between these domains, and process composition is interpreted by a trace operator. We illustrate our semantics by validating expected program equivalences.
