New technicl report

[Matthew Hennessy]

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 -------