[Prev][Next][Index][Thread]
two technical reports
I would like to bring to the attention of subscribers to the types
mailing list two technical reports on the use of type systems in
concurrency theory. Both are available from
http://www.cogs.susx.ac.uk/
Cheers
Matthew Hennessy
================================================================
1. The security picalculus and non-interference
by
Matthew Hennessy
University of Sussex Technical Report 2000:05
Abstract:
The security picalculus is a typed version of the asynchronous
picalculus in which the types, in addition to constraining the
input/output behaviour of processes, have security levels associated
with them. This enables us to introduce a range of typing disciplines
which allow input or output behaviour, or both, to be bounded above
or below by a given security level. We define typed versions of may
and must equivalences for the security picalculus, where the tests
are parameterised relative to a security level. We provide alternative
characterisations of these equivalences in terms of actions in
context; these describe the actions a process may perform in a given
typing environment, assuming the observer is constrained by a
related but possibly different environment. The paper also contains
non-interference results with respect to may and must testing.
These show that certain form of non-interference can be enforced
using our typing systems.
2. Typed behavioural equivalences for processes in the presence
of subtyping
by
Matthew Hennessy and Julian Rathke
University of Sussex Technical Report 2001:02
Abstract:
We study typed behavioural equivalences for the picalculus, in
which the type system allows a form of subtyping. This enables
processes to selectively distribute different capabilities on
communication channels. The equivalences considered include
typed versions of testing equivalences and barbed bisimulation
equivalences. We show that these can be characterised via standard
techniques applied to a novel labelled transition system of
configurations. These consist of a process term together with two
related type environments; one constraining the process and the
other its computing environment