A new proposal of Concurrent Process Calculus^{⋆}

Salvador Lucas and Javier Oliver

Departamento de Sistemas Informáticos y Computación Universidad Politécnica de Valencia Camino de Vera s/n, Apdo. 22012, 46020 Valencia, Spain. e.mail:{slucas,joliver}@dsic.upv.es

Abstract. In this paper, we present a new calculus to model concurrent systems, the Parallel Label-Selective λ-calculus. This calculus integrates the (functional) expressiveness of the λ-calculus in a unified framework with some powerful features for expressing communication actions and supporting the independence of processes which can be a main source of improvement when performing parallel computations.

Keywords: Concurrency, Extensions of λ-calculus, Functional Programming, Process Algebra.

1 Introduction

A computational model links the software and hardware description levels of computer systems, in order to analyze the correctness, completeness or efficiency of programs which we want to run on a given machine. General agreement seems to exist on the main features that a model of concurrency should include: a concurrent system is a community of sequential processes which can work in an independent or interdependent fashion [3]. Concurrency and communication express independency and interdependency: concurrent processes (independently) deal with their respective tasks until a cooperation (i.e., a communication) is needed. Functional languages provide an excellent tool for parallel computation because there are no side-effects. Functional programs can be evaluated sequentially or in parallel without changing their denotational or declarative semantics. Nevertheless, the inclusion of constructs for explicit concurrency enhances the expressiveness of executable specification languages as there are programs which can best be described as a composition of parallel processes [8]. Sequential (functional) computation is traditionally captured by the λ-calculus [2] as Berry showed in [4]. Function declarations and their application to data (which can eventually be other functions) is supported by the language. Thus, an important challenge for researchers was to find a framework for the concurrency and the communication between processes similar to the λ-calculus, [1, 5, 7, 10, 11].

We introduce the Parallel Label-Selective λ-calculus, LCEP^{2}, to model concurrency and communication from a functional perspective. The expressiveness of the λ-calculus is integrated within a unified framework with powerful features to explicitly express the communication actions and the independence of processes, which are the main source of improvements when performing parallel computations. Since our framework originates from the λ-calculus, we chose a

⋆ This work has been partially supported by CICYT, TIC 95-0433-C03-03. 2 λ-Cálculo Etiquetado Paralelo.

functional point of view to describe concurrency. The basic feature of functional programming is the application of functions to values. In this setting, communication can be viewed as argument instantiation, if we embed the adequate means to provide ‘remote’ instantiation of parameters. The formal parameter takes the role of a communication channel. The need for an ordered matching of the formal and actual parameters is also relaxed to bring up the necessary independence of parallel systems. This allows us to speak of the sequential application of a function to its parameters instead of the standard application, and the parallel application of a function to remote, possibly committing parameters which in this case models the standard communication. The idea of how long and to what extent a remote parameter can be instantiated in a function call is captured by means of the notion of tunnel, which is novel in the literature.

This paper is organized as follows: Section 2 describes the language and the reduction system of the calculus. Section 3 gives a general idea of using LCEP as a target language to mechanize functional concurrent languages. The last section offers some conclusions and suggestions for future work.

2 The calculus

LCEP is a calculus which originated from a previous proposal by H. Aït-Kaci, the Label-Selective λ-calculus [1], an extension of the λ-calculus in which function arguments are selected by labels. Symbolic and numeric labels can be used to name the communication channels. This has not been possible in other proposals and permits the use of currying and labeled specification of parameters. It makes the ordering of the actual parameters in a function call independent of the presentation order of the formal parameters in the definition.

Example 1 Let f = λxy.x − y be a λ-term. In LCEP, we can define the function f as f(p, q) = λ_{p}x.λ_{q}y.x − y. We name the formal parameters of f by means of labels p, q. We can specify the application of f to parameters a, b by giving its destination in two ways: by explicitly indicating either the number of the formal parameters, f(b → 2, a → 1) = f(a, b), or the name of the formal parameters, f(b → q, a → p) = f(a, b).

However, the Label-Selective λ-calculus is not very appropriate for concurrency: it lacks both a non-deterministic choice and explicit parallelism operators. The calculus supports concurrency among different channels, but it is not able to describe, for example, alternative choices over the same channel. For instance, the dining philosophers problem, cannot be modeled using Label-Selective λcalculus because non-deterministic choice and parallelism operators are both needed [12]. They are introduced by following Milner’s π-calculus [11].

2.1 Description of LCEP

Let V = {x, y, z, …} be a set of variables, and C = {a, b, c, …} be a set of constants. P represents a channel name from a set of labels L = IN ∪ S, where m, n, … denote numerical labels taken from IN (the set of natural numbers), S = {p, q, …} is a set of symbolic labels, and IN ∩ S = ∅. Constants, variables and the null process (denoted by 0) form the atomic elements of the language. The language of the formal system that we present is M. It is defined as follows:

M ::= 0 | a | x | λ_{P} x.M | _{P}M | (M ∥ M) | (M ∘ M) | (M + M) | !M

P ::= number | symbol

In concurrent programming, the terms M ∈ M represent processes. Symbols ∘ (sequential composition), ∥ (parallel composition), + (nondeterministic choice) and ! (replication) are considered as process constructors. The operators λ_{P} x (abstraction or input) and _{P} (parameter passing or output) are also considered as process constructors, whose effect over a process M is to define processes (λ_{P} x.M and _{P}M, respectively) which are involved in functional applications under certain given conditions. We consider a partial order relation, ⪯_{L} on L. The numerical label 0 is the minimum of this poset. By analogy with λ-calculus, the process constructors can be viewed as symbols of a signature [9], that is, a set of function symbols, each of which has a fixed arity. Symbols ∘, ∥, + are binary operations, !, λ_{P} x and _{P} are unary operations for all P ∈ L and x ∈ V, x, 0 are 0-ary operations for all x ∈ V and we let P = {_{P} : P ∈ L} and Λ = {λ_{P} x : (P ∈ L) ∧ (x ∈ V)} be the set of output and input operations, respectively. The terms of this signature are called λ_{∥}-terms.

We use the habitual notions of occurrence, set of occurrences, subterm, etc. (see [6] for complete definitions). Terms are viewed as labeled trees in the usual way. Occurrences u, v, … are chains of positive natural numbers used to address subterms of t. They are ordered by: u ≤ v, if ∃w. u.w = v. We let u | v iff u ≰ v and v ≰ u. O(t) denotes the set of occurrences of a term t. t|_{u} is the subterm at an occurrence u of t. t[s]_{u} is the term t with the subterm at the occurrence u replaced with s. t[u] denotes the symbol which labels the root of t|_{u}.

[figure: N; M; _{P}; λ_{P} x; ∥]

Fig. 1. Syntactical tree of the process λ_{P} x.M ∥ _{P}N

In the tree representation of a λ_{∥}-term A, a tuple γ = ⟨u_{1}, …, u_{n}⟩, u_{i} ∈ O(A) for 1 ≤ i ≤ n is a path between the subprocesses M = A|_{u} and N = A|_{v} (u, v disjoint occurrences), if γ is the shortest path in A verifying u_{1} = u′ and u_{n} = v′ whenever u = u′.i and v = v′.j for some i, j ∈ IN. We associate to the path of occurrences γ the path γ^{s} = ⟨s_{1}, …, s_{n}⟩ of symbols s_{i} = A[u_{i}] rooted at these occurrences. For the sake of expressiveness, we usually identify γ^{s} and γ. For example, in Figure 1 the path between the processes M and N is ⟨λ_{P} x, ∥, _{P}⟩.

The symbol ≡ represents the least congruence over M, satisfying the following properties [11]: (M/ ≡, ∥, 0) and (M/ ≡,+, 0) are commutative monoids, M ∘ 0 = 0 ∘ M ≡ M (identity), !M ≡ M ∥ !M, and _{0}M ≡ M.

2.2 Reduction system

Reductions between processes are defined by an Inference System.

Axioms: First, β_{sec} and β_{P} model the different kinds of application.

1. β_{sec}: β sequential application:

(… + λ_{P} x.M) ∘ (_{P}N ∘ L + …) →_{β_{sec}} M[N/x] ∘ L where P ∈ L − {0}

2. β_{P}: β parallel application, through the argument labeled with channel P:

(… + λ_{P} x.M) ∥ (_{P}N ∘ L + …) →_{β_{P}} M[N/x] ∥ L where P ∈ L − {0} and

β_{P} is a family of rules indexed by L − {0}.

β_{sec} models the standard side-by-side application of a function to its arguments. A β_{P} rule expresses the ‘parallel’ application of a function to (possibly many) committing arguments (on the same channel or name-of-formal-parameter). Therefore, β_{P} expresses the classical communication process on a channel P, which can also be viewed from a functional perspective.

Now the reordering rules extend the corresponding rules of the Label-Selective λ-calculus. They manage currying and unordered specification of arguments to a function (Example 1).

1. Reordering with numeric labels. Let m, n ∈ IN − {0}, L, M, N ∈ M, x, y ∈ V: η_{1} : (λ_{m}x.λ_{n}y.M) →_{η_{1}} (λ_{n}y.λ_{m−1}x.M) if m ≻_{L} n

η_{2} : _{m}M ∘ _{n}N →_{η_{2}} _{n}N ∘ _{m−1}M if m ≻_{L} n

η_{sec_{3}} : (… + λ_{m}x.M) ∘ (_{n}N ∘ L + …) →_{η_{sec_{3}}} λ_{m−1}x.(M ∘ _{n}N) ∘ L if m ≻_{L} n

η_{sec_{4}} : (… + λ_{m}x.M) ∘ (_{n}N ∘ L + …) →_{η_{sec_{4}}} λ_{m}x.(M ∘ _{n−1}N) ∘ L if m ≺_{L} n

2. Reordering with symbolic labels. Let p, q ∈ S, L, M, N ∈ M, x, y ∈ V: ρ_{1} : (λ_{p}x.λ_{q}y.M) →_{ρ_{1}} (λ_{q}y.λ_{p}x.M) if p ≻_{L} q

ρ_{2} : _{p}M ∘ _{q}N →_{ρ_{2}} _{q}N ∘ _{p}M if p ≻_{L} q

ρ_{sec_{3}} : (…+λ_{p}x.M)∘(_{q}N∘L+…) →_{ρ_{sec_{3}}} λ_{p}x.(M∘_{q}N)∘L if (p ≻_{L} q) ∨ (p ≺_{L} q)

Rules: The structural inference rules are the following:

\begin{matrix}μ_{∘_{1}} : & \frac{M → M′}{M ∘ N → M′ ∘ N} & μ_{∘_{2}} : & \frac{M → M′}{N ∘ M → N ∘ M′} \\ μ_{λ} : & \frac{M → M′}{λ_{P} x.M → λ_{P} x.M′} & μ : & \frac{M → M′}{_{P}M → _{P}M′} \\ μ_{∥} : & \frac{M → M′}{M ∥ N → M′ ∥ N} & μ_{Congr} : & \frac{M ≡ N N → N′ N′ ≡ M′}{M → M′} \end{matrix}

2.3 The concept of tunnel We interpret the syntactical structure of the process as the ‘physical’ means within which communication among the subprocesses is established. From this point of view, β_{P} application describes the communication between two communicating processes, λ_{P} x.M and _{P}N, on channel P linked by a single constructor of parallelism (∥). From the functional point of view, this can be thought of as the remote instantiation of the actual parameter N in the body M of a function through the formal parameter P. We extend the scope of this simplest ‘remote’ binding by our notion of tunnel. For example, in Figure 1, λ_{P} x.M and _{P}N communicate (using channel P) through the (shortest) tunnel ⟨ ∥ ⟩. We extend the scope of β_{P} communication by means of the tunnel rule:

μ_{T} : \frac{M ∥ N →_{β_{P}} M′ ∥ N′}{_{Q_{1}}M ∥ _{Q_{2}}N →_{β_{P}} _{Q_{1}}M′ ∥ _{Q_{2}}N′} for Q_{1}, Q_{2} ∈ L if P ≻_{L} Q_{1}, Q_{2}

μ_{T} expresses the possibility of β_{P} communication between processes M and N, provided the following conditions are met: [T1] M and N are able to establish a β_{P} communication, [T2] _{Q_{1}}M and _{Q_{2}}N are compound in parallel, and [T3] the label P ∈ L is greater than labels Q_{1} and Q_{2}.

T1 is obviously necessary to make any communication feasible. T2 motivates the definition of a syntactic object, namely the tunnel. It is possible to formalize it as a (special kind of) path in the syntactical tree of a process.

Definition 2.1 (Tunnel) Let A be a λ_{∥}-term. An elemental path in the syntactical tree of A, γ = ⟨u_{1}, …, u_{n}⟩, u_{i} ∈ O(A), for 1 ≤ i ≤ n is a tunnel iff, n > 1 ⇒ u_{1} | u_{n} and, being γ^{s} = ⟨s_{1}, …, s_{n}⟩, s_{i} ∈ {∥} ∪ P for i 1 ≤ i ≤ n, and there is j, 1 ≤ j ≤ n such that s_{j} = ∥. Definition 2.2 (Tunnel location) Given a tunnel γ = ⟨u_{1}, …, u_{n}⟩ in a λ_{∥}- term A, the tunnel location ν_{γ} is the least occurrence of the elemental path of the tunnel: ν_{γ} = min{u_{i} | 1 ≤ i ≤ n}. Note that A[ν_{γ}] = ∥.

Example 2 In the syntactical tree of C ≡ _{Q_{1}}A ∥ _{Q_{2}}(A_{1} ∥ B), we identify a tunnel.

[figure: B; A_{1}; ∥; A; _{Q_{2}}; _{Q_{1}}; ∥]

Fig. 2. Tunnel between processes A and B We are going to verify that, if A ≡ λ_{P} x.M and B ≡ _{P}N, then a β_{P} communication

is possible between A and B, in C. We assume that P ≻ Q_{i} for i = 1, 2.

(1) A ∥ B →_{β_{P}} A′ ∥ B′ A and B definition

(2) A ∥ A_{1} ∥ B →_{β_{P}} A′ ∥ A_{1} ∥ B′ μ_{∥_{1}}

(3) _{Q_{1}}A ∥ _{Q_{2}}(A_{1} ∥ B) →_{β_{P}} _{Q_{1}}A′ ∥ _{Q_{2}}(A_{1} ∥ B′) μ_{T}

In the syntactical tree of process C, ⟨_{Q_{1}}, ∥, _{Q_{2}}, ∥⟩ is a tunnel between nodes A and B.

Having a tunnel between a sender and a receiver is not sufficient to get communication. Condition T3 motivates the definition of transparency of a tunnel. Definition 2.3 (P -transparent tunnel) Given a label P ∈ L, a tunnel γ = ⟨u_{1}, …, u_{n}⟩ is P -transparent if, being γ^{s} = ⟨s_{1}, …, s_{n}⟩, for all i, 1 ≤ i ≤ n,

s_{i} ≠ ∥ ⇒ P ≻_{L} Q_{i}, where s_{i} = _{Q_{i}}.

Definition 2.4 (T -communicability) Let A be a λ_{∥}-term, M = A|_{u} be a sender and N = A|_{v} be a receiver on a channel P. They are T -communicable on P if:

1. There exists a P -transparent tunnel γ between M and N.

2. Let ν_{γ} the location of γ. Then, ∀w ∈ O(A) : w ≤ ν_{γ} ⇒ A[w] ∈ {∥, ∘}∪Λ∪P. Thus, parallel communication is a particular T -communication in which the tunnel between the communicating processes is the simplest one: γ = ⟨∥⟩. From the definition of tunnel transparency, it follows that, for all P ∈ L, γ is always P -transparent.

3 Mechanizing functional concurrent languages using LCEP

In this section, we illustrate the ability of LCEP for mechanizing a functional concurrent language. A functional program F is a set of function definitions. Its execution is the evaluation of an expression E. Thus, the two main challenges are the modelling of function definitions and the modelling of the evaluation of expressions^{3}.

Modelling function definitions. In a functional program, a k-ary (userdefined) function F can be specified as follows: def F (x_{1}, …, x_{k}) = E_{F}. Formal parameters are named x_{1}, …, x_{k} and the expression E_{F} describes the ‘actions’ performed by F. E_{F} is an expression in which calls to other functions can be found: basic functions from B_{1}, …, B_{m} (for instance, if, +, ∗), user-defined functions from F_{1}, …, F_{n} (even the same F function in recursive definitions).

A program with a goal expression E is translated into a λ_{∥}-term M = M_{B} ∥ M_{F} ∥ M_{E}. It contains the representation of the basic functions M_{B}, the program representation M_{F} and the representation of the expression to be evaluated M_{E}. The process M_{B} is M_{B} = M_{B_{1}} ∥ ⋯ ∥ M_{B_{m}}, where M_{B_{i}} corresponds to the basic function B_{i}. M_{F} is M_{F} = M_{F_{1}} ∥ ⋯ ∥ M_{F_{n}}, where M_{F_{i}} corresponds to the user-defined function F_{i}. M_{E} is τ[E], where the translation function τ, mapping sentences of the language into λ_{∥}-expressions is defined below.

The structures of M_{B_{i}} 1 ≤ i ≤ m and M_{F_{j}} 1 ≤ j ≤ n are similar. We translate a (general) function definition def H(x_{1}, …, x_{k}) = E_{H}, where H can be a basic or user-defined function, into a λ_{∥}-term M_{H} as follows:

- M_{H} =!_{H}A_{H}. A_{H} is the abstraction of the function H. By using the function name H as a communication channel, we enable the communication mechanism to ‘send’ the abstraction of H to the place where it is needed. By prefixing with the ! operator, we are able to obtain as many copies of A_{H} as necessary.

- A_{H} = λ_{1}x′_{1}. · · · .λ_{1}x′_{k}.S_{H} has two parts. The first one (λ_{1}x′_{1}. · · · .λ_{1}x′_{k}.) is devoted to receiving the arguments for the second one, S_{H}, which translates the expresion E_{H}.

- Basic and user-defined functions differ in the way that the process S_{H} is defined. A basic function B is predefined: we let S_{B} = C_{B} ∘x′_{1}∘⋯∘x′_{k}, where C_{B} ∈ C is a constant expressing the basic function. The evaluation of LCEP expressions involving these constants is managed in a special manner as we show below.

- On the other hand, S_{F} = τ[E_{F}] for user-defined functions F. Therefore, S_{F} only represents the process which evaluates the expression E_{F} defining F.

We complete the definition of the translation function τ as follows^{4}:

Translation of expressions. An expression E is always viewed as a function call E = F (E_{1} → j_{1}, …, E_{k} → j_{k}). E_{i} → j_{i} means that the i-th real parameter E_{i} corresponds to the j_{i}-th formal parameter of F. Since the calculus expresses concurrency, the evaluation of a function call starts with the parallel evaluation of the actual parameters:

- τ[E] = M_{Arg} ∥ M_{Ap}. The evaluation of E splits up into two parts: the process evaluating the arguments, M_{Arg}, and the process which performs the application of the function to the (evaluated) arguments, M_{Ap}.

- M_{Ap} = λ_{σ_{1}}σ′_{1}. · · · .λ_{σ_{k}}σ′_{k}.λ_{F} F′.F′ ∘_{1}σ′_{1} ∘⋯∘_{1}σ′_{k}. Application of the function F

consists in first receiving the (evaluated) arguments E_{1}, …, E_{k} through channels σ_{1}, …, σ_{k}, next, receiving the abstraction of F through the channel F and then,

3 For reasons of brevity, the development is somewhat informal. We do not start from a real language, but rather from general sentences which have a syntax which is similar to almost every functional language.

4 In a more complete treatment, we would be able to introduce many other features to increase parallelism.

applying it to the arguments. The labels σ_{i} are considered to be fresh.

- M_{Arg} = _{σ_{1}}τ[E_{1}] ∥ ⋯ ∥ _{σ_{k}}τ[E_{k}]. For each real parameter E_{i}, we build an evaluation environment^{5} _{σ_{i}}τ[E_{i}] for the process τ[E_{i}] that represents the expression to evaluate. They are transparent for global scope processes but they are not transparent for the local processes.

Therefore, the activation mechanism begins building an execution environment for each formal parameter and then communicates the final result through the channels σ_{i}. When the function arguments are evaluated, the execution continues applying the function definition over them.

The ordering of labels is essential in this scheme. We define the ordering ⪯_{L} adequately to deal with these requirements. In the set of symbolic labels, we state σ |_{L} σ′, H |_{L} H′ and σ ≺_{L} H for all labels σ, σ′ used in evaluation environments and basic or user-defined functions H, H′. The set of numeric labels inherits the standard ordering on IN. This definition of the order ⪯_{L} is also essential in managing recursivity.

Modelling the evaluation of expressions. Similar to the usual practice in implementing pure functional languages [13], the execution of the process M on LCEP is composed of mixed steps. The different reduction rules apply in this precedence order:

1. Evaluation rules defined for the basic functions: +, −, etc.^{6}

2. Reordering rules,

3. Sequential application and

4. Extended parallel β-application, i.e. T -communication. β_{H} communications are (equally) prioritary for all basic or user-defined function H. Tunnels located at outermost positions are (equally) prioritary.

Evaluation rules are associated to basic functions. For example, denote as P LUS and MINUS the LCEP constants associated to the functions + and −. Assuming that A, B are numbers, we have the following built-in evaluation rules: P LUS ∘ A ∘ B →_{eval_{P LUS}} A + B and MINUS ∘ A ∘ B →_{eval_{MINUS}} A − B.

Example 3 Let F be defined by def F (x, y) = x − y (as in Example 1). The

associated process is M_{F} =! _{F}λ_{1}x.λ_{1}y.λ_{MINUS}MINUS′.MINUS′ ∘ _{1}x ∘ _{1}y. Proc-

esses M_{P LUS} and M_{MINUS} are: M_{P LUS} = ! _{P LUS}(λ_{1}x_{1}.λ_{1}x_{2}.P LUS ∘ x_{1} ∘ x_{2}), and

M_{MINUS} = ! _{MINUS}(λ_{1}x_{1}.λ_{1}x_{2}.MINUS ∘ x_{1} ∘ x_{2}). Since !M ≡ M ∥ !M (see Section

2.1), we have the necessary copies of the processes.

The evaluation of E = F (1 + 1 → 2, 3 + 3 → 1) is the execution of:

M_{E} = τ[F (1 + 1 → 2, 3 + 3 → 1)] = λ_{σ_{1}}σ′_{1}.λ_{σ_{2}}σ′_{2}.λ_{F} F′.(F′ ∘ _{2}σ′_{1} ∘ _{1}σ′_{2}) ∥

∥ _{σ_{1}}(λ_{P LUS}P LUS′.(P LUS′ ∘ _{1}1 ∘ _{1}1)) ∥

∥ _{σ_{2}}(λ_{P LUS}P LUS′.(P LUS′ ∘ _{1}3 ∘ _{1}3))

as follows: M_{P LUS} ∥ M_{MINUS} ∥ M_{F} ∥ M_{E}

In contrast to the λ-calculus where the abstractions must be kept in an environment for use when they are needed, in LCEP it is possible to completely express the program as a term of the calculus.

5 In some cases, we simplify the expression of M_{Ap} and M_{Arg} by avoiding useless

evaluations of the basic expressions: variables and constants (see below). 6 Since LCEP includes the λ-calculus, it would be possible to express these opera-

tions as λ_{∥}-expressions, by defining the natural numbers and operations as λ-terms. However, this is not used in real implementations and so we follow this standard approach.

4 Conclusions and future work

LCEP has been presented in this paper. It is an extension of the λ-calculus to model concurrent systems. In our framework, communication is viewed as a special kind of function application. We distinguish between sequential and parallel application of functions to arguments. The tunnel concept is introduced to relate remote arguments and function abstractions. Also, one of the new features in relation to previous proposals is to allow the function arguments to be selected by means of both symbolic and numerical labels, which permits the use of currying. We are building a prototype of an abstract machine based on the formal system described here to execute programs written in a high-level language that allows us to express explicit parallelism.

References

1. H. Aït-Kaci and J. Garrigue. Label-Selective λ-Calculus: Syntax and Confluence. In R. K. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 761 of LNCS, pages 24–40. Springer-Verlag, Berlin, 1993.

2. H.P. Barendregt. The λ-calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier Science Publishers, 1984 edition, Amsterdam, 1991.

3. M. Ben-Ari. Principles of Concurrent Programming. Englewood Cliffs: Prentice Hall, 1982.

4. G. Berry. Séquentialité de l’évaluation formelle des λ-expressions. In Proc. of 3-e Colloque International sur la Programmation, Dunod, Paris 1978.

5. G. Berry and G. Boudol. The Chemical Abstract Machine. In Proc. of 20’th ACM Annual Symp. on Principles of Programming Languages, pages 81–93, ACM Press, 1993.

6. N. Dershowitz and J.P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 243–320. Elsevier, Amsterdam and the MIT Press, Cambridge, MA., 1990.

7. C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall International, Great Britain, 1985.

8. M.P. Jones and P. Hudak. Implicit and explicit parallel programming in Haskell. Technical report, YALEU/DCS/RR-982, Yale University, New Haven, Connecticut, USA, August 1993.

9. R. Lalement. Computation as Logic. Prentice Hall International, Great Britain, 1993.

10. R. Milner. A Calculus of Communicating Systems. LNCS 92, 1980. Springer Verlag.

11. R. Milner. The polyadic π-calculus: A tutorial. In F.L. Brauer, W. Bauer, and H. Schwichtenberg, editors, Logic and Algebra of Specifications. Springer-Verlag, Berlin, 1993.

12. J. Oliver and S. Lucas. Survey of concurrent calculi. In M.A. Fernández, J.M. García, J.A. Guerrero, and G. Moreno, editors, Nuevas tendencias en la Informática: Arquitecturas Paralelas y Programación Declarativa, pages 267–289, 1994.

13. S.L. Peyton-Jones. The implementation of functional programming languages. Prentice Hall International, Great Britain, 1987.

This article was processed using the L^{A}TEX macro package with LLNCS style