A BRICS Mini-Course
November 12, 18, 20 and 23, 1998
School of Cognitive and Computing Sciences, University of Sussex, UK
The lectures will examine a formal language for describing widely distributed open systems where mobile agents can move from site to site seeking resources and effecting computations. We will principally be concerned with type systems for such agents which guarantee no misuse of local resources, even in the presence of agents which may harbour malicious intentions.
The language, Dpi, is obtained by adding to the pi-calculus new constructs for located processes and process migration. The type system is based on the notion of a location type, which describes the set of resources (channels) available to an agent at a location. Resources are themselves equipped with capabilities, and thus an agent may be given permission to send data along a channel at a particular location without being granted permission to read data along the same channel.
In the presence of potentially malicious agents we show that the integrity of local resources can still be maintained by incorporating various forms of type checking into the runtime semantics.
The general research area of professor Matthew Hennessy may be described as the semantic foundations of programming and specification languages. He is particularly interested in distributed computing, including mobile computing. He is also interested in the development of verification tools.