[Prev][Next][Index][Thread]
New technical report
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
The following Technical Report makes extensive use of types to
control the behvaiour of mobile code; it should therefore be of
interest to the subscribers to this mailing list.
It is available from
http://cogslib.cogs.susx.ac.uk/csr.php?type=cs
===============================================================
Title: SafeDpi: a language for controlling mobile code
Author(s): Matthew Hennessy, Julian Rathke, Nobuko Yoshida
Report: Computer Science Report 2003:02
Issued: University of Sussex, Brighton BN1 9QH, October 2003
Abstract: SafeDpi is a distributed version of the picalculus, in which
processes are located at dynamically created sites.
Parametrised code may be sent between sites using so-called
ports, which are essentially higher-order versions of
picalculus communication channels. A host location may
protect itself by only accepting code which conforms to a
given type associated to the incoming port. We define a
sophisticated static type system for these ports, which
restrict the capabilities and access rights of any processes
launched by incoming code. Dependent and existential types
are used to add flexibility, allowing the behaviour of these
launched processes, encoded as process types, to depend on
the host's instantiation of the incoming code. We also show
that a natural contextually defined behavioural equivalence
can be characterised coinductively, using bisimulations
based on typed actions. The characterisation is based on the
idea of knowledge acquisition by a testing environment and
makes explicit some of the subtleties of determining
equivalence in this language of highly constrained
distributed code.
------- end of forwarded message -------