Functions as Session-Typed Processes
Functions as Session-Typed Processes
复制标题
作为会话类型进程的函数
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
F. Pfenning
中科院分区：
文献类型：
--
作者：
Bernardo Toninho;Luís Caires;F. Pfenning
我们研究了在会话类型的π-calculus中简单类型的λ-calculus的类型编码。我们在先前的工作中表明了线性扣除的线性扣除，如何将线性序列中的证据解释为π-calculus toge toce typline toge表明由此产生的翻译会影响原始λ-Terms的共享和复制并行评估策略，从而为这些策略提供了新的逻辑动机解释。
We study type-directed encodings of the simply-typed λ-calculus in a session-typed π-calculus. The translations proceed in two steps: standard embeddings of simply-typed λ-calculus in a linear λ-calculus, followed by a standard translation of linear natural deduction to linear sequent calculus. We have shown in prior work how to give a Curry-Howard interpretation of the proofs in the linear sequent calculus as π-calculus processes subject to a session type discipline. We show that the resulting translations induce sharing and copying parallel evaluation strategies for the original λ-terms, thereby providing a new logically motivated explanation for these strategies.