[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