[Prev][Next][Index][Thread]
Typing and Subtyping for the Mobile Processes
The following paper is now available for anonymous FTP. Retrieval
instructions follow the abstract.
Cheers,
Benjamin Pierce
Davide Sangiorgi
----------------------------------------------------------------------
TYPING AND SUBTYPING FOR MOBILE PROCESSES
Benjamin Pierce and Davide Sangiorgi
The pi-calculus is a process algebra that supports process mobility by
focusing on the communication of channels.
Milner's presentation of the pi-calculus includes a type system
assigning arities to channels and enforcing a corresponding discipline
in their use. We extend Milner's language of types by distinguishing
between the ability to read from a channel, the ability to write to a
channel, and the ability both to read and to write. This refinement
gives rise to a natural subtype relation similar to those studied in
typed lambda-calculi.
The greater precision of our type discipline yields stronger versions
of some standard theorems about the pi-calculus. These can be used,
for example, to obtain the validity of beta-reduction for the more
efficient of Milner's encodings of the call-by-value lambda-calculus,
for which beta-reduction does not hold in the ordinary pi-calculus.
We define the syntax, typing, subtyping, and operational semantics of
our calculus, prove that the typing rules are sound, apply the system
to Milner's lambda-calculus encodings, and sketch extensions to
higher-order process calculi and polymorphic typing.
----------------------------------------------------------------------
Retrieval instructions:
ftp ftp.dcs.ed.ac.uk [or 129.215.160.5]
login: anonymous
password: <your mail address>
cd pub/bcp
binary [don't forget this!]
get pi.dvi