π演算的资源分析
A resource analysis of the pi-calculus
摘要：
本文在分离逻辑语义理论的基础上，继续Hoare和O 'Hearn的研究计划，给出了π演算的一种新的处理方法。使用一种新的资源模型，区分公共和私人所有权，我们重构的操作语义，使发送，接收和分配的命令，影响拥有的资源。这些想法自然会导致两个指称模型：一个是安全性模型，一个是活性模型。这两个模型都是完全抽象的相应的可观测量，但更重要的是，两者都非常简单。与分离逻辑的模型理论（特别是与布鲁克斯的行动轨迹模型）的密切联系产生了过程和资源的逻辑。
英文摘要：
We give a new treatment of the pi-calculus based on the semantic theory of separation logic, continuing a research program begun by Hoare and O'Hearn. Using a novel resource model that distinguishes between public and private ownership, we refactor the operational semantics so that sending, receiving, and allocating are commands that influence owned resources. These ideas lead naturally to two denotational models: one for safety and one for liveness. Both models are fully abstract for the corresponding observables, but more importantly both are very simple. The close connections with the model theory of separation logic (in particular, with Brookes's action trace model) give rise to a logic of processes and resources.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
