Part I
Nobuko Yoshida
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 with 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 guarantee 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. In Part II, we present uniform
type-based static analyses of two basic security concerns for the
typed calculus, secrecy for data confidentiality and access controls
for authorised resources. Part III uses this framework for developing
and justifying a type discipline for a simple multi-threaded
class-based language with distributed code mobility which guarantees
secrecy and safe access to resources.