Communication errors in the pi-calculus are undecidable
We present an undecidability proof of the notion of communication errors in the polyadic pi-calculus. The demonstration follows a general pattern of undecidability proofs-reducing a well-known undecidable problem to the problem in question. We make use of an encoding of the lambda-calculus into the pi-calculus to show that the decidability of communication errors would solve the problem of deciding whether a lambda term has a normal form. (C) 1999 Elsevier Science B.V. All rights reserved.
concurrency programming calculi program correctness