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

Cliff Jones has proposed transformations between concrete programs and general transformation rules that increase concurrency in a system of objects, and has raised the challenge of how to prove their validity. We present a proof 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 channels 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 processed using the same continuation. This work is also intended as an example of the usefulness of pi-calculus types for reasoning. (C) 1999 John Wiley & Sons, Inc.