University of Sussex
Browse

File(s) under permanent embargo

safeDpi: a language for controlling mobile code.

chapter
posted on 2023-06-07, 14:10 authored by Matthew Hennessy, Nobuko Yoshida, Julian Rathke
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 hostrsquos 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.

History

Publication status

  • Published

Journal

FoSSaCS

Publisher

Springer, Verlag

Volume

2987

Page range

241-256

Pages

529.0

Book title

Foundations of Software Science and Computation Structures

ISBN

9783540212980

Series

Lecture Notes in Computer Science

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Editors

Igor Walukiewicz

Legacy Posted Date

2008-02-29

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC