The receptive distributed π-calculus

We study an asynchronous distributed π-calculus, with constructs for localities and migration. We show that a static analysis ensures the receptiveness of channel names, which, together with a simple type system, guarantees the message deliverability property. This property states that any migrating...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on programming languages and systems 2003-09, Vol.25 (5), p.549-577
Main Authors: Amadio, Roberto M., Boudol, Gérard, Lhoussaine, Cédric
Format: Article
Language:English
Subjects:
Computer Science
Logic in Computer Science
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We study an asynchronous distributed π-calculus, with constructs for localities and migration. We show that a static analysis ensures the receptiveness of channel names, which, together with a simple type system, guarantees the message deliverability property. This property states that any migrating message will find an appropriate receiver at its destination locality. We argue that this distributed, receptive calculus is still expressive enough while allowing for an effective type inference à la ML.
ISSN:0164-0925
1558-4593
DOI:10.1145/937563.937564