论文标题
渴望用作过程（长版）
Eager Functions as Processes (long version)
论文作者
论文摘要
我们将米尔纳（Milner）编码逐价$λ$ -calculus，以$π$ -calculus的形式进行编码。我们表明，通过将编码调整为两个$π$ -calculus（内部$π$和异步的本地$π$）的两个子calculi，这是由编码与Lassen的急切的bisimrility相同的$λ$ terms的等价。作为$π$ -calculus中的行为等价性，我们考虑上下文等价和刺刺的一致性。我们还将结果扩展到预订。证明中的至关重要的技术成分是最近引入的独特方程解决方案技术，这是本文进一步开发的。在这方面，本文还打算是有关该技术的适用性和表现力的扩展案例研究。
We study Milner's encoding of the call-by-value $λ$-calculus into the $π$-calculus. We show that, by tuning the encoding to two subcalculi of the $π$-calculus (Internal $π$ and Asynchronous Local $π$), the equivalence on $λ$-terms induced by the encoding coincides with Lassen's eager normalform bisimilarity, extended to handle $η$-equality. As behavioural equivalence in the $π$-calculus we consider contextual equivalence and barbed congruence. We also extend the results to preorders. A crucial technical ingredient in the proofs is the recently-introduced technique of unique solutions of equations, further developed in this paper. In this respect, the paper also intends to be an extended case study on the applicability and expressiveness of the technique.
