Graph Types for Monadic Mobile Processes

Nobuko Yoshida


While types for name passing calculi have been studied extensively in the context of sorting of polyadic pi-calculus, the type abstraction on the corresponding level is not possible in the monadic setting, which was left as an open issue by Milner. We solve this problem with an extension of sorting which captures dynamic aspects of process behaviour in a simple way. Equationally this results in the full abstraction of the standard encoding of polyadic pi-calculus into the monadic one: the sorted polyadic pi-terms are equated by the basic behavioural equality in the polyadic calculus if and only if their encodings are equated in the basic typed behavioural equality in the monadic calculus. This is the first result of this kind we know of in the context of the encoding of polyadic name passing, which is a typical example of translation of high-level communication structures into pi-calculus. The construction is general enough to be extensible to encodings of calculi with more complex operational structures.


This report is available in the following formats:

Previous | Index | Next