[Prev][Next][Index][Thread]
Types in Monadic Mobile Processes
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The following paper is available by anonymous ftp on the site:
ftp.dcs.ed.ac.uk/export/ny/pub/graph1.ps.Z
-------------------------------------------------------------------
Graph Types for Monadic Mobile Processes
by
Nobuko Yoshida
(Edinburgh University)
*** Abstract ***
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 [Milner 92]. 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
extendable to encodings of calculi with more complex operational
structures.
[Milner 92] Milner, R., Polyadic $\pi$-Calculus: a tutorial. Logic and
Algebra of Specification, Springer-Verlag, 1992.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Any comments are welcome.
Nobuko Yoshida
******************************************
* Nobuko Yoshida *
* *
* Department of Computer Science *
* University of Edinburgh *
* address: The King's Buildings *
* Mayfield Road *
* Edinburgh UK EH9 3JZ *
* tel: 44-131-650-4889 (direct) *
* fax: 44-131-667-7209 *
* E-mail: ny@dcs.ed.ac.uk *
******************************************