Typed pi-calculus at work: A correctness proof of Jones's parallelisation transformation on concurrent objects

Cliff Jones has proposed transformations between concrete programs and gene ral transformation rules that increase concurrency in a system of objects, and has raised the challenge of how to prove their validity. We present a p roof of correctness of the hardest of Jones's concrete transformations. The proof uses a typed pi-calculus and typed behavioral equivalences. Our type system tracks receptiveness; it guarantees that the input-end of certain c hannels is always ready to receive messages (at least as long as there are processes that could send such messages), and that all messages will be pro cessed using the same continuation. This work is also intended as an exampl e of the usefulness of pi-calculus types for reasoning. (C) 1999 John Wiley & Sons, Inc.