Typed π‐calculus at work: A correctness proof of Jones's parallelisation transformation on concurrent objects
1999; Wiley; Volume: 5; Issue: 1 Linguagem: Inglês
10.1002/(sici)1096-9942(199901/03)5
ISSN1096-9942
Autores Tópico(s)Logic, Reasoning, and Knowledge
ResumoCliff 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 π-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 π-calculus types for reasoning. © 1999 John Wiley & Sons, Inc.
Referência(s)