π-演算十三问 FAQ on π-Calculus

原文：https://www.cs.cmu.edu/~wing/publications/Wing02a.pdf

π-演算十三问 FAQ on π-Calculus

Jeannette M. Wing
微软研究院访问研究员 Visiting Researcher, Microsoft Research
卡内基梅隆大学计算机科学教授 Professor of Computer Science, Carnegie Mellon University

2002 年 12月 27 日 27 December 2002

1. 何为 π-演算？ What is π-calculus?

π-演算是并发系统的计算模型。
π -calculus is a model of computation for concurrent systems.

π-演算的语法允许表示过程，过程的并行组合，过程之间透过通道来同步通信，新过程的创建，过程的复制和非确定性。如此而已！
The syntax of π-calculus lets you represent processes, parallel composition of processes, synchronous communication between processes through channels, creation of fresh channels, replication of processes, and nondeterminism. That’s it!

2. 过程是什么意思，通道又是什么意思? What do you mean by process? By channel?

过程是独立控制线程的抽象。通道是两个过程之间通信链接的抽象。过程透过通道发送和接收消息来相互交互。
A process is an abstraction of an independent thread of control. A channel is an abstraction of the communication link between two processes. Processes interact with each other by sending and receiving messages over channels.

3. 能更具体一点吗？Could you be a little more concrete?

P 和 Q 表示过程。然后 • P | Q 表示由 P 和 Q 并行运行着所组成的那个过程。
Let P and Q denote processes. Then • P | Q denotes a process composed of P and Q running in parallel.

• a(x).P 表示等待从通道 a 读取值 x 的过程，然后收到该值，表现如 P。
• a(x).P denotes a process that waits to read a value x from the channel a and then, having received it, behaves like P.

• ā〈x〉.P 表示首先等待沿通道 a 发送值为 x 的过程，然后在某些输入过程接受 x 之后，表现如 P。
• ā〈x〉.P denotes a process that first waits to send the value x along the channel a and then, after x has been accepted by some input process, behaves like P.

• (νa)P 确保 a 是 P 中的新通道（将希腊字母 “nu” 读作“new”。）
• (νa)P ensures that a is a fresh channel in P. (Read the Greek letter “nu” as “new.”)

• !P 表示 P 有无限的拷贝，全部并行运行。
• !P denotes an infinite number of copies of P, all running in parallel.

• P + Q 表示行为类似 P 或 Q 的过程。
• P + Q denotes a process that behaves like either P or Q.

• 0 表示无效的过程。
• 0 denotes the inert process that does nothing.

你可以想象的所有并发行为都必须依据上述结构去编写。All concurrent behavior that you can imagine would have to be written in terms of just the above constructs.

4. 举个例子怎么样？ （我怕不耐烦的读者可能会跳过这个问题。）How about an example? (Impatient readers should feel free to skip this question.)

假设你要在客户端和服务器之间建立远程方法调用。考虑在服务器上运行的以下函数 incr()。incr() 返回大于其参数 x 1的整数：
Suppose you want to model a remote procedure call between a client and a server. Consider the following function, incr, running on the server. incr returns the integer one greater than its argument, x:

int incr(int x) { 
	return x+1;
} 

首先，我们将服务器的 “incr” 建模为 π 演算中的一个过程，如下所示：
First, we model the “incr” server as a process in π-calculus as follows:

!incr(a, x).ā〈x+1〉 

先忽略 ！ 符号，这个过程表达式表示 incr 通道接受两个输入：一个是通道的名称，a，我们将用它来返回调用 incr 的结果，另一个是参数 x，它会在客户端调用的时候被实例化为整数值。调用之后过程将在通道 a 上发回增加其参数 x 的结果。在上面的过程表达式中使用了复制操作符，意味着 “incr” 将很乐意为自己制作多个副本，每个客户端交互一个副本。
Ignoring the ! for now, this process expression says that the incr channel accepts two inputs: one is the name of the channel, a, which we will use to return the result of calling incr, and the other is the argument, x, which will be instantiated with an integer value upon a client call. After the call, the process will send back the result of incrementing its argument, x, on the channel a. The use of the replication operator, !, in the above process expression means that the “incr” server will happily make multiple copies of itself, one for each client interaction.

现在我们模拟一个客户端调用 “incr”服务端。 在以下赋值语句中，输入 17 得到 incr 的结果绑定到整数变量 y：
Now let’s model a client call to the “incr” server. In the following assignment statement, the result of calling incr with 17 gets bound to the integer variable y:

y := incr(17) 

在 π-演算中像是会这样： and would look like this in π-calculus:

 (νa)( incr〈a, 17〉 | a(y) ) 

按并行方式说，就是：（1）在 incr 通道上发送通道 a（用于传回结果值）和整数值 17，（2）然后在通道 a 上接收结果 y。通过 ν 运算符可确保为每个客户端与 “incr” 服务端之间能够建立专用通信通道来相互交互。
which says in parallel: (1) send on the incr channel both the channel a (for passing back the result value) and the integer value 17, and (2) receive on the channel a the result y. The use of the ν operator guarantees that a private channel of communication is set up for each client interaction with the “incr” server.

将客户端和服务器进程并行放在一起，我们得到最终的过程表达式：
Putting the client and server processes in parallel together we get the final process expression:

!incr(a, x).ā〈x+1〉 |  (νa)( incr〈a, 17〉 | a(y) ) 

表示客户端使用参数17 调用“incr”服务器，并将返回值 18 分配给 y。
which expresses the client call to the “incr” server with the argument 17 and the assignment of the returned value 18 to y.

5. π 演算和λ 演算有什么区别与联系？ What is the analogy between π-calculus and λ-calculus?

λ-演算是顺序过程的程序，而 π 演算是并发程序。
λ-calculus is to sequential programs as π-calculus is to concurrent programs.

更确切地说，λ 演算是函数计算的核心语言，其中“一切都是函数”，所有计算都是通过函数程序进行的; π 演算是基于消息的并发的核心演算，其中“一切都是过程”，所有计算都是透过通道上的通信进行的。λ 演算可以声称是函数计算的规范模型；然而，π 演算不能对并发计算提出那样的要求[Pierce95]。
More precisely, λ-calculus is the core language of functional computation, in which “everything is a function” and all computation proceeds by function application; π-calculus is the core calculus of message-based concurrency, in which “everything is a process” and all computation proceeds by communication on channels. λ-calculus can claim to be a canonical model of functional computation; however, π-calculus cannot make such a claim for concurrent computation [Pierce95].

本杰明·皮尔斯说得最好：Benjamin Pierce puts it best:

lambda-calculus 拥有令人羡慕的力量：简言之，它具备了函数计算的所有基本特征。此外，函数计算的其他基础，如图灵机，具有完全相同的表达能力。lambda 演算的“必然性”源于以下事实：观察函数计算的唯一方法是当呈现不同输入值时观测它产生哪些输出值。
The lambda-calculus holds an enviable position: it is recognized as embodying, in miniature, all of the essential features of functional computation. Moreover, other foundations for functional computation, such as Turing machines, have exactly the same expressive power. The “inevitability” of the lambda-calculus arises from the fact that the only way to observe a functional computation is to watch which output values it yields when presented with different input values.

不幸的是，并发计算的世界并不是那么有序。被观察到的不同概念可能适用于不同的情况，从而对两个并发系统何时具有“相同行为”产生不同的定义：例如，我们可能希望观察或忽略系统的固有并行度，情况它可能会陷入僵局，在物理处理器之间分配其进程，或者它对各种故障的恢复能力。此外，并发系统可以用许多不同的构造来描述，用于创建进程（fork / wait，cobegin / coend，future，data parallelism等），在它们之间交换信息（共享内存，集合点，消息传递，数据流，等），并管理他们对共享资源（信号量，监视器，交易等）的使用。
Unfortunately, the world of concurrent computation is not so orderly. Different notions of what can be observed may be appropriate for different circumstances, giving rise to different definitions of when two concurrent systems have “the same behavior”: for example, we may wish to observe or ignore the degree of inherent parallelism of a system, the circumstances
under which it may deadlock, the distribution of its processes among physical processors, or its resilience to various kinds of failures. Moreover, concurrent systems can be described in terms of many different constructs for creating processes (fork/wait, cobegin/coend, futures, data parallelism, etc.), exchanging information between them (shared memory, rendezvous, message-passing, dataflow, etc.), and managing their use of shared resources (semaphores, monitors, transactions, etc.).

这种可变性引发了一大类称为过程演算（有时是过程代数）的正式系统，每个系统都体现了特定并发或分布式编程范式的本质[Pierce 95]。
This variability has given rise to a large class of formal systems called process calculi (sometimes process algebras), each embodying the essence of a particular concurrent or distributed programming paradigm [Pierce 95].

π 演算只是众多此类过程演算中的一种。
π-calculus is just one of many such process calculi.

有趣的是：λ 演算可以用 π 演算编码。
An interesting aside: λ-calculus can be encoded in π-calculus.

6. 为什么有时会使用“过程代数”这个术语？ 什么是过程代数？ Why is the term “process algebra” sometimes used? What is a process algebra?

代数是一种数学结构，具有一组值和对值的一组操作。 这些操作享有代数性质，如交换性，相关性，幂等性和分布性。 在典型的过程代数中，过程是值，并行组合被定义为对过程的交换和关联操作。
An algebra is a mathematical structure with a set of values and a set of operations on the values. These operations enjoy algebraic properties such as commutativity, associativity, idempotency, and distributivity. In a typical process algebra, processes are values and parallel composition is defined to be a commutative and associative operation on processes.

7. π 演算与其前身过程演算有什么区别？What’s the difference between π-calculus and its predecessor process calculi?

π 演算与早期过程演算的区别 - 特别是罗宾米尔纳自己在传播系统计算（CCS）[Milner80] 和 Tony Hoare 关于传递顺序过程（CSP）[Hoare85 ] 有相似工作 - 将频道传递为 其他通道的数据。 此功能允许你表达过程移动性，从而允许表达过程结构中的更改。 例如，假设你在驾车时正在用手机通话；对过程移动性进行建模的能力对于描述手机在此过程中与不同基站的通信方式非常有用。
What distinguishes π−calculus from earlier process calculi—in particular Robin Milner’s own work on Calculus of Communicating Systems (CCS) [Milner80] and Tony Hoare’s similar work on Communicating Sequential Processes (CSP) [Hoare85]—is the ability to pass channels as data along other channels. This feature allows you to express process mobility, which in turn allows you to express changes in process structure. For example, suppose you’re talking on your cell phone while driving in your car; the ability to model process mobility is useful for describing how your phone communicates with different base stations along the way.

8. 能用π演算编程吗？Can you program in π-calculus?

是的，但你不想。
Yes, but you wouldn’t want to.

就像 λ 演算可被视为顺序程序的汇编语言一样，并发程序的 π 演算也是如此。两者都是简单，灵活，高效实现，适合编译更高级语言功能的目标 [Pierce95]。但是，将两者用作源级编程语言都是不切实际的。例如，如果您的并发编程模型基于共享内存，就像所有 Threads 库一样，那么根据通道编码每个全局共享变量将是麻烦的。
Just as λ-calculus can be viewed as an assembly language for sequential programs, so can π-calculus for concurrent programs. Both are simple, flexible, efficiently implementable, and suitable targets for compilation of higher-level language features [Pierce95]. But both would be impractical to use as a source-level programming language. For example, if your concurrent programming model is based on shared memory, as is the case with all Threads libraries, then encoding each globally shared variable in terms of channels would be cumbersome.

相反，π 演算最好被用于为高级并发或分布式编程语言提供底层语义的正式框架。例如，Jim Larus，Sriram Rajamani 和 Jakob Rehof 根据 π 演算[LRR02] 设计了用于异步编程的新语言， Sharpie。
Rather, π-calculus is best viewed as a formal framework for providing the underlying semantics for a high-level concurrent or distributed programming language. For example, Jim Larus, Sriram Rajamani, and Jakob Rehof give the semantics of their new Sharpie language, for asynchronous programming, in terms of π-calculus [LRR02].

根据 π 演算或其他过程演算定义其语义的语言，包括较旧的 Pict [PierceTurner97]，Amber [Cardelli86]，Concurrent ML [Reppy91] 和 Facile [Amadio94]。值得注意的是，尽管这些语言比 π 演算更高级，但实际上并没有使用它们。 （相比之下，在顺序编程领域，Scheme，ML 和 Haskell是 三种流行的函数式编程语言，其语义由 λ 演算构建 - 所有这三种语言在教学和研究中都被广泛使用。）
Older languages that define their semantics in terms of π-calculus or other process calculi include Pict [PierceTurner97], Amber [Cardelli86], Concurrent ML [Reppy91], and Facile [Amadio94]. Notably, even though these languages are higher-level than π-calculus, none of them are used in practice. (In contrast, in the sequential programming world, Scheme, ML, and Haskell are three popular functional programming languages whose semantics build from λ-calculus—all three are used widely in teaching and in research.)

9. π 演算作为实用工具有什么用？ What good is π-calculus as a practical tool?

π 演算，或任何过程演算，都可以作为建模语言。
π-calculus, or any process calculus for that matter, is good as a modeling language.

特别是，人们已经成功地使用过程计算来建模协议。毕竟，协议描述了过程应该相互通信的方式。人们已经使用过程计算来建模和验证电信协议，通常得到模型检查工具的支持，例如 Concurrency Workbench [CPS93] 和 FDR [FDR93]。其他人使用 π 演算变体，称为 Spi 演算，来推理密码协议[AbadiGordon97]。
In particular, people have successfully used process calculi to model protocols. Protocols, after all, describe ways in which processes should communicate with each other. People have used process calculi to model and verify telecommunications protocols, often with support from model checking tools such as the Concurrency Workbench [CPS93] and FDR [FDR93]. Others have used a π-calculus variant, called Spi-calculus, to reason about cryptographic protocols [AbadiGordon97].

与使用任何建模语言一样，模型和代码之间仍然存在巨大差距，即在期望行为的规范与实现它的程序之间。您可以优化模型，直到吐出“正确”的代码，或者编写代码并证明其对模型的“正确性”。两种方法都有不同程度的自动化支持，以获得不同程度的成功。如何缩减这一差距仍有待该领域的研究。
As with using any modeling language, there still remains a huge gap between the model and the code, i.e., between the specification of desired behavior and the program that implements it. Either you refine your model till you spit out “correct” code or you write code and prove its “correctness” against your model. Both approaches are used, with varying degrees of automated support, to varying degrees of success. Attacking this gap is still an active area of research.

为了说明这个差距有多大，请再次考虑问题四中远程过程调用的建模。RPC 的实现必须考虑诸如编组和解组参数和结果之类的细节，处理诸如链接或服务器故障之类的故障，同步时钟，优先定位服务器等等。显然，在理解高级协议的情况下，您只对各种客户端和服务器之间的交互感兴趣（例如，通过在线旅行社进行预订的用户），您希望忽略该级别的详细信息。在这里，作为建模语言的 π-演算是一种胜利。但是，最终你不仅要实现 RPC，还要实现特定于应用程序的协议（例如，旅行者不应该重复预订）。如何保证正确实现了 RPC 等通信协议以及特​​定于应用程序的协议仍是一个难题。
To illustrate how large this gap can be, consider again the modeling of remote procedure call in Question 4. An implementation of RPC would have to consider details such as marshalling and unmarshalling arguments and results, handling failures such as links or servers going down, synchronizing clocks, locating the server in the first place, and so on. Clearly, at a level of understanding a high-level protocol, where you are interested in only the interactions between various clients and servers (e.g., users making reservations through an on-line travel agency), you want to ignore that level of detail. Here, π-calculus as a modeling language is a win. But, eventually you have to implement not just RPC, but also the application-specific protocol (e.g., travelers should not double book). How to guarantee you have correctly implemented your communications protocol such as RPC as well as your application-specific protocol is still a hard problem.

10. π 演算，或者更普遍的过程演算，与软件工程有什么关系？ What does π-calculus, or more generally process calculi, have to do with software engineering?

过程计算最近在软件工程研究中发挥作用的一个地方是软件架构领域。软件体系结构描述系统的组件（例如，客户端和服务器，对等进程，分布式代理）和连接器（例如，远程过程调用，事件广播，发布 - 订阅，Unix 管道）。连接器描述组件通信的协议。Rob Allen 和 David Garlan 定义了一种名为 Wright [AllenGarlan97] 的软件架构语言，适用于定义不同类型的连接器，即组件可以交互的不同方式。他们用 CSP[Hoare95] 来表达 Wright 的语义，CSP 是与 CCS（π 演算的前身）在同一系列中的一个过程代数。此外，他们使用 FDR 模型检查器[FDR93]，其语义也是根据 CSP 的，用于查找软件系统的体系结构级描述中的错误。
One place where process calculi have recently played a role in software engineering research is in the field of software architecture. A software architecture describes a system’s components (e.g., clients and servers, peer processes, distributed agents) and connectors (e.g., remote procedure call, event broadcast, publish-subscribe, Unix pipes). A connector describes the protocol by which components communicate. Rob Allen and David Garlan define a software architecture language called Wright [AllenGarlan97], suitable for defining different kinds of connectors, i.e., different ways in which components can interact. They give the semantics of Wright in terms of CSP [Hoare95], a process algebra in the same family as CCS, the predecessor of π-calculus. Moreover, they use the FDR model checker [FDR93], whose semantics are also given in terms of CSP, to find bugs in architecture-level descriptions of software systems.

11. .π 演算作为一种形式主义有什么用呢？ What good is π-calculus as a formalism?

与任何形式主义一样，π-演算可以帮助回答看上去完全不同但却基本一致的问题，所有问题都在一个框架内完成。例如，考虑一下同步与异步通信。打个电话是一个同步通信的例子；发送电子邮件是异步通信的一个例子。
π-calculus, as with any formalism, can help answer fundamental questions about seemingly disparate issues, all within a single framework. For example, consider synchronous versus asynchronous communication. Making a telephone call is an example of synchronous communication; sending e-mail is an example of asynchronous communication.

同步 π 演算要求发送者和接收者在通信时会合。异步是分布式系统中固有的，因为消息从一台机器传输到另一台机器需要时间。因此许多研究人员使用异步 π 演算作为他们的并发模型，它是同步 π 演算的一个片段，特别是对于分布式计算的建模。
Synchronous π-calculus requires that senders and receivers rendezvous when communicating. Asynchrony is inherent in distributed systems, because it takes time for a message to travel from one machine to another. Thus, many researchers use asynchronous π-calculus, which is a fragment of synchronous π-calculus, as their model of concurrency, especially for modeling distributed computation.

一个自然产生的问题是这两种机制是否相同，即可以实现另一种吗？众所周知，如何在同步方面实现异步通信。但另一个方向呢？ Catuscia Palamidessi 使用 π 演算作为统一框架来回答这个问题：同步沟通更加强大 [Palamidessi02]。
A question that naturally arises is whether these two mechanisms are equivalent, i.e., can one implement the other? It is well known how to implement asynchronous communication in terms of synchronous. But what about the other direction? Catuscia Palamidessi uses the π-calculus as a uniform framework to answer this question in the negative: synchronous communication is more powerful [Palamidessi02].

12. 为什么有这么多形式主义，如 π 演算和抽象状态机（ASM）？ Why are there so many formalisms such as π-calculus and Abstract State Machines (ASM)?

有很多种形式主义。它们适合描述的系统类型（例如，硬件，实时，程序，协议），它们可用于证明的属性类型（例如，正确性，死锁自由，时间，活性），在它们的基础逻辑能力（例如，一阶，高阶），它们的基础语义模型（例如，代数结构的类型），它们的可用性（例如，表达能力，工具支持，可伸缩性）等中 π-演算是描述通过消息传递进行通信的并发进程的自然选择。它不是描述抽象数据类型的适合选择。描述具有丰富或复杂数据结构的状态不是适合的选择。
There are many classes of formalisms. They differ in the types of systems they are suitable for describing (e.g., hardware, real-time, programs, protocols), in the types of properties they can be used to prove (e.g., correctness, deadlock freedom, timing, liveness), in their underlying logical power (e.g., first-order, higher-order), in their underlying semantic model (e.g., type of algebraic structure), in their usability (e.g., expressive power, tool support, scalability), etc. π-calculus is a natural choice for describing concurrent processes that communicate through message passing. It is not a natural choice for describing abstract data types. It is not a natural choice for describing states with rich or complex data structures.

ASM 是描述抽象状态和改变状态的单步转换的自然选择。它的并发模型基于抽象共享全局状态。有关 ASM 相关论文，请参阅Yuri Gurevich 的网站 http://research.microsoft.com/~gurevich/annotated.html，包括 Lipari 1993 指南（＃103），它根据演化代数定义顺序，并行和分布式 ASM [Gurevich93]。
ASM is a natural choice for describing abstract states and single-step transitions that change state. Its model of concurrency is based on abstract shared global state. See Yuri Gurevich’s web site http://research.microsoft.com/~gurevich/annotated.html for ASM-related papers, including the Lipari 1993 guide (#103) that defines sequential, parallel, and distributed ASMs in terms of evolving algebras [Gurevich93].

有关其他形式主义的大量信息，请参阅http://archive.comlab.ox.ac.uk/formal-methods.html：其注释，方法和工具。截至今天，π-演算和 ASM 是所列出的 92 个中的两个。
See http://archive.comlab.ox.ac.uk/formal-methods.html for a wealth of information about other formalisms: their notations, methods, and tools. As of today, π-calculus and ASM are two of the 92 listed.

13. 我在哪里可以阅读更多关于π演算的内容？ Where can I read more about π-calculus?

关于 π 演算的标准参考文献是米尔纳的教程 《ThePolyadicπ-calculus》[Milner91]、米尔纳和 Walker 的两部分文章《移动过程的演算》[MPW92]、米尔纳的书《传播和移动系统：π-演算》[Milner99]、Sangiorgi 和 Walker 对研究生的教材《π演算：移动过程理论》[SangiorgiWalker01]，里面对 λ演算中的 π 演算给出了详细的编码，并展示了如何在 π 演算中进行面向对象编程。

Benjamin Pierce对 λ 演算和 π 演算都给出了很好的介绍[Pierce95]。

有关移动过程计算的参考书目，请参见http://liinwww.ira.uka.de/bibliography/Theory/pi.html。

Standard references on π-calculus are Milner’s tutorial “The Polyadic π-calculus” [Milner91]; Milner, Parrow, and Walker’s two-part article “A Calculus of Mobile Processes” [MPW92]; and Milner’s book, Communicating and Mobile Systems: the
π-calculus [Milner99]. Sangiorgi and Walker’s graduate-level textbook, The π-calculus: A Theory of Mobile Processes [SangiorgiWalker01], gives a detailed encoding of λ-calculus in π-calculus and shows how to do object-oriented programming in π-calculus.

Benjamin Pierce gives an excellent introduction [Pierce95] to both λ-calculus and π-calculus.

See http://liinwww.ira.uka.de/bibliography/Theory/pi.html for a bibliography on calculi for mobile processes.

致谢 Acknowledgments
感谢 Jim Larus，Dan Ling 和 Jim Kajiya 的一般性评论。 感谢吉姆 Larus 特别建议，他添加了问题二，以及 Jakob Rehof 和 Sriram Rajamani 就问题四的例子给予了帮助。感谢 Yuri Gurevich 帮助了我对 ASM 的理解，他的指针说明很有用。问题五中的回答其实很多都来自本杰明皮尔斯的 CRC 手册文章[Pierce95]。

I thank Jim Larus, Dan Ling, and Jim Kajiya for their general comments. Thanks to Jim Larus for his specific suggestion to add Question 2, and to Jakob Rehof and Sriram Rajamani for their help with the example for Question 4. Thanks to Yuri Gurevich for clarifying my understanding of ASMs and for his helpful pointers. I took most of the answer in Question 5 from Benjamin Pierce’s CRC Handbook article [Pierce95].

引用 References

[AbadiGordon97] Martin Abadi and Andrew Gordon, Reasoning about Cryptographic Protocols in the Spi Calculus, CONCUR’97: Concurrency Theory, Lecture Notes in Computer Science, volume 1243, Springer-Verlag, July 1997, pp. 59-73.
http://research.microsoft.com/~adg/Publications/details.htm

[AllenGarlan97] Robert Allen and David Garlan, A Formal Basis for Architectural Connection, ACM Trans. on Soft. Eng. and Methodology, July 1997.
http://www-2.cs.cmu.edu/afs/cs.cmu.edu/project/able/www/paper_abstracts/wright-tosem97.html

[Amadio94] Roberto M. Amadio, Translating core Facile, Technical Report ECRC-TR-3-94, European Computer-Industry Research Center, GmbH, Munich, 1994.

[Cardelli86] Luca Cardelli, Amber, Combinators and Functional Programming Languages, Lecture Notes in Computer Science, volume 242, Springer-Verlag, 1986, pp.
21-47.

[CPS93] Rance Cleaveland, Joachim Parrow, and Bernhard Steffen, The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems, ACM Trans. on Prog. Lang. and Systems, 15(1): 36-72, January 1993.
http://www.cs.sunysb.edu/~rance/publications/./1993.html

[FDR93] Formal Systems (Europe) Ltd., Failures-Divergences-Refinement, User Manual and Tutorial, 1993.

[Gurevich93] Yuri Gurevich, Evolving Algebras 1993: Lipari Guide, in Specification and Validation Methods, ed. E. Börger, Oxford University Press, 1995, pp. 9-36.
http://research.microsoft.com/~gurevich/Opera/103.pdf

[Hoare85] C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.

[LLR02] Jim Larus, Sriram Rajamani, and Jakob Rehof, Behavioral Types of Asynchronous Programming, Microsoft Research Technical Report, November 2002, submitted to PLDI.
http://www.research.microsoft.com/behave/sharpie-report-abs.html

[Milner80] Robin Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, volume 92, Springer-Verlag, 1980.

[Milner91] Robin Milner, The Polyadic π-calculus, Technical Report ECS-LFCS-91-180, Lab. for Foundations of Computer Science, Dept. of Computer Science, University of Edinburgh, UK, October 1991.
http://www.lfcs.informatics.ed.ac.uk/reports/91/ECS-LFCS-91-180/

[Milner99] Robin Milner, Communicating and mobile systems: the π-calculus, Cambridge University Press, 1999.

[MPW92] Robin Milner, Joachim Parrow, and David Walker, A Calculus of Mobile Processes, Parts I and II, Information and Computation, 100(1): 1-40 and 41-77.
http://www.lfcs.informatics.ed.ac.uk/reports/89/ECS-LFCS-89-85/

http://www.lfcs.informatics.ed.ac.uk/reports/89/ECS-LFCS-89-86/

[Palamidessi02] Catuscia Palamidessi, Comparing the Expressive Power of the Synchronous and the Asynchronous π-calculi, to appear in Math. Struct. in Comp. Sci., 2002.
http://www.cse.psu.edu/~catuscia/papers/pi_calc/mscs.ps

[Pierce95] Benjamin C. Pierce, Foundational Calculi for Programming Languages, CRC Handbook of Computer Science and Engineering, Chapter 136, CRC Press, 1996.
http://www.cis.upenn.edu/~bcpierce/papers/

[PierceTurner97] Benjamin C. Pierce and David N. Turner, Pict: A Programming Language Based on the Pi-Calculus, Indiana University CSCI Technical Report #476, 1997.
http://www.cis.upenn.edu/~bcpierce/papers/

[Reppy91] John Reppy, CML: A higher-order concurrent language, Proc. of Programming Language Design and Implementation, ACM SIGPLAN, June 1991, pp. 293-259.

[SangiorgiWalker01] Davide Sangiorgi and David Walker, The π-calculus: a Theory of Mobile Processes, Cambridge University Press, 2001.