SPEAKER:
Matthew Hennessy, Univ. of Sussex

TITLE: Typed equivalences for the picalculus,
joint work with Julian Rathke

Reference: Typed behavioural equivalences in the Picalculus.
University of Sussex Technical Report csr2001:02
Latest version available from
http://www.cogs.susx.ac.uk/users/matthewh


ABSTRACT:

The talk will discuss the impact which types play on the standard behavioural theory of the
(asynchronous) picalculus.

We first review the behavioural theory of the untyped language, in
particular the relationship between bisimulations and contextual
equivalences.

We next give a `capability-based` type system for the picalculus, with
which resource access control policies can be modelled. The general
idea is that names of resources are no longer sent and received by
processes; instead restricted capabilities on resource names can by
selectively distributed by using typed communication.

Finally we show that the presence of these types affect the notion of
when systems should be considered behaviourally equivalent.  Typed
bisimulation equivalences are developed and, as in the untyped case,
can be justified contextually.