[moca] Channel Dependent Types for Higher-Order Mobile Processes

[Nobuko Yoshida <yoshida@xxxxxxxxxxxx>]

The following paper is available.

I am grateful for any comments, suggestions and remarks.

-----------------------------------------------------
Channel Dependent Types for Higher-Order Mobile Processes

(Part I)

http://www.doc.ic.ac.uk/~yoshida/paper/partI.ps

Nobuko Yoshida (yoshida@xxxxxxxxxxxx)

We introduce a new expressive theory of types for the higher-order
pi-calculus which significantly improves our previous work presented
in [Yoshida and Hennessy 2000] by the use of channel
dependent/existential types. New dependent types control dynamic
change of process accessibility via channel passing, while existential
types guarantee safe scope-extrusion in higher-order process
passing. This solves an open issue in [Yoshida and Hennessy 2000],
leading to significant enlargement of original typability and offering
a general basis for analysing and verifying higher-order mobile
computation. This paper establishes a basic theory of dependent and
existential types for the higher-order pi-calculus, and coherently
integrates the resulting formalism with the linear/affine typing
disciplines as well as state, concurrency and distribution, which
allow precise embedding of major language constructs in the
calculus. The type discipline can guarantee unique accessibility of
resources, termination of migrating code, a response property from a
remote server and encapsulation of higher-order code by hidden
names. The technical development in this paper gives a firm basis for
the applications discussed in its sequels.


 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html