In this chapter we look at type systems for the language aPi. The traditional view of types is that they provide an aid to programmers to avoid runtime errors during the execution of programs. We start with this view, explaining what runtime errors might occur during the execution of aPi processes, and design a type system that eliminates the possibility of such errors.

We then modify the set of types, so that they implement a more subtle notion of resource access control. Here the resources are simply channels, and the more subtle type system enables access to these resources to be managed; that is read and write accesses can be controlled. The view taken is that one no longer programs directly with resource names. Instead programming is in terms of capabilities on these names, the ability to read to or write from a particular resource. These capabilities are managed by the owners of resources and may be selectively distributed to be used by other processes.

Runtime errors

The traditional use of types and type checking is to eliminate runtime errors in highlevel programs. Specifically types are annotations inserted into the program text by the program designer, or inferred automatically by a type inference system, which indicate the intended use of various resources. Then prior to execution the annotated program is typechecked, that is syntactically analysed, to ensure that the behaviour of the program will indeed respect the intended use of these resources.

From ATM machines dispensing cash from our bank accounts, to online shopping websites, interactive systems permeate our everyday life. The underlying technology to support these systems, both hardware and software, is well advanced. However design principles and techniques for assuring their correct behaviour are at a much more primitive stage.

The provision of solid foundations for such activities, mathematical models of system behaviour and associated reasoning tools, has been a central theme of theoretical computer science over the last two decades. One approach has been the design of formal calculi in which the fundamental concepts underlying interactive systems can be described, and studied. The most obvious analogy is the use of the λ-calculus as a simple model for the study of sequential computation, or indeed the study of sequential programming languages. CCS (a Calculus for Communicating Systems) [28] was perhaps the first calculus proposed for the study of interactive systems, and was followed by numerous variations. This calculus consists of:

• A simple formal language for describing systems in terms of their structure; how they are constructed from individual, but interconnected, components.

• A semantic theory that seeks to understand the behaviour of systems described in the language, in terms of their ability to interact with users.

Here a system consists of a finite number of independent processes that intercommunicate using a fixed set of named communication channels. This set of channels constitutes a connection topology through which all communication takes place; it includes both communication between system components, and between the system and its users.

Throughout the book we will make extensive use of both induction and coinduction, and their associated proof techniques. Here we give a brief review of these concepts, and an indication of how we intend to use them.

Induction

Figure 1.1 contains a definition of the (abstract) syntax of a simple language of machines. Here a ranges over some set of action labels Act, and intuitively a machine can carry out sequences of these actions, and periodically has a choice of which actions to perform. Let M be the set of all machines defined in Figure 1.1. Formally this is an inductive definition of a set, namely the least set S that satisfies

• stop ∈ S

• M ∈ S implies a.M ∈ S for every action label a in Act

• M1, M2 ∈ S implies M1 + M2 ∈ S.

The fact that M is the least set that satisfies these conditions gives us a proof technique for defining and proving properties of machines in M; any other set satisfying the conditions is guaranteed to contain M.

As an example consider the following definition of the size of a machine:

• |stop| = 0

• |a.M| = 1 + |M|

• |M1 + M2| = |M1| + |M2|.

We know by induction that this function is now defined for every machine. Belabouring the point for emphasis let D be the domain of the size function | |, the set of elements for which it is defined.

Here we describe a simple language in which values are exchanged between concurrent processes via communication channels. These channels can be used to model resources and the syntax allows them to be declared as private, for the exclusive shared use of specific processes. The names of these channels/resources can also be transmitted between processes, resulting in a very powerful descriptive language.

We give two different views of the language. The first, via a reduction semantics, describes how processes may evolve. This may be seen as a specification of an interpreter for the language and is taken to be the primary semantic definition. The second view is an action semantics, which describes how processes can interact with other processes, perhaps as part of a larger system; this describes how processes can behave as part of a larger endeavour. This second view interprets the language as a labelled transition system or lts, as explained in Definition 1.2, and thus induces automatically a bisimulation equivalence between processes.

The language aPi

The syntax of the language aPi is given in Figure 2.1. It presupposes a set Names of names, ranged over by n,m, …, a, b, c … for communication channels or resources. We also use a set Vars of variables, place-holders for values that can be transmitted via the communication channels. These values will include some unspecified collection of base values such as integers, booleans, strings, etc., ranged over by bv, but more importantly channel names themselves.

In this chapter we apply the theory developed for aPi in Chapter 4 to aDpi. For technical reasons it is best to work relative to the extended typing system developed in Section 5.5, although to avoid unnecessary clutter we will abbreviate ⊢rc to simply ⊢.

The motivation for this theory, the relativisation of behavioural equivalences to the partial knowledge of observers as explained in Chapter 4, applies equally well, if not more so, in a distributed setting. Consequently it is not repeated here. Moreover the technical framework, developed in detail in Chapter 4, is easily adapted to aDpi. So we simply apply it, modifying the various concepts as necessary to the distributed setting, in what we hope is a natural manner.

In the first section we discuss distributed actions-in-context and the associated typed bisimulation equivalence, ≈bis, for aDpi systems. Most proofs of the expected properties of this equivalence are left to the reader as they can be easily constructed from the corresponding ones in Sections 4.1 and 4.2.

This is followed by a section on examples, which demonstrates that at least in principle standard bisimulation-based proof methodologies can be adapted to our setting. Necessarily there are more syntactic details to contend with; but in time appropriate software tools, based for example on theorem provers, could be developed to partially alleviate the tedium.

In the final section we revisit the subject first broached in the untyped setting of aDpi, in Section 2.5, namely the justification of our typed bisimulation equivalence for aDpi.