Author name cluster

Samuel Hym

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

I&C Journal 2009 Journal Article

Mobility control via passports

Samuel Hym

Dπ is a simple distributed extension of the π-calculus in which agents are explicitly located, and may use an explicit migration construct to move between locations. In this paper, we introduce passports to control those migrations; in order to gain access to a location agents are now expected to show some credentials, granted by the destination location. Passports are tied to specific locations, from which migration is permitted. We describe a type system for these passports, which includes a novel use of dependent types, and prove that well-typing enforces the desired behaviour in migrating processes. Passports allow locations to control incoming processes. This induces major modifications to the observations which can be made of agent-based systems. Using the type system we describe these observations, and use them to build a loyal notion of observational equivalence for this setting. Finally we provide a complete proof technique in the form of a bisimilarity for establishing equivalences between systems.

Details DOI

TCS Journal 2007 Journal Article

Adding recursion to Dpi

Samuel Hym
Matthew Hennessy

Dpi is a distributed version of the pi-calculus, in which processes are explicitly located, and a migration construct may be used for moving between locations. We argue that adding a recursion operator to the language increases significantly its descriptive power. But typing recursive processes requires the use of potentially infinite types. We show that the capability-based typing system of Dpi can be extended to co-inductive types so that recursive processes can be successfully supported. We also show that, as in the pi-calculus, recursion can be implemented via iteration. This translation improves on the standard ones by being compositional but still requires co-inductive types and comes with a significant migration overhead in our distributed setting.

Details DOI