Type systems for the ambient calculus.

[23,8] and [38,4] consider the Ambient Calculus, proposed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code, and develop type systems for the calculus. These systems employ a notion of causality in that processes are assigned “behaviors”, where a behavior is essentially a regular set of traces. Thus type checking (of fully annotated processes) is decidable, using techniques borrowed from finite automata theory. (Under certain restrictions, type inference is also possible.)

In [23], the focus is on extending the ambient calculus so as to allow a more natural, yet safe, style of programming. This is done by embedding a functional language, and by designing the type system to smoothly integrate several kinds of “polymorphism”: (i) the well-investigated notion of subtyping; (ii) “arity polymorphism”, allowing the same ambient to hold several topics of conversation simultaneously; and (iii) “orderly communication”, allowing the same ambient to hold several topics of conversation consecutively. A subject reduction property ensures that communicating subprocesses agree on their “topic of conversation”. As “orderly communication” is the main technical innovation of the above, the journal paper [8] concentrates on this feature only.

In [38], summarized and put into perspective in [4], the focus is on security in that the type system is parameterized by a set of security constraints: static ones expressing where a given ambient may reside, and dynamic ones expressing where a given ambient may be dissolved. A subject reduction property then guarantees that a well-typed process never violates these constraints. It is argued that the presence of causality significantly increases the precision of the analysis and compensates for the lack of “co-capabilities” (an otherwise increasingly popular extension to the ambient calculus).

The goal of [36], and the further development in [21], is to provide type polymorphism of the kind that is usually present in polymorphic type systems for the lambda-calculus, thereby allowing mobile agents to follow non-predetermined paths and to carry non-predetermined types of data from location to location. This is achieved by letting the type of an ambient process give an upper bound on the possible ambient nesting shapes of any process to which it can evolve. Because these shapes can depend on which capabilities and names are actually communicated, the types support this with explicit dependencies on communication. The type of an ambient name may thus depend on where the ambient has traveled, whereas in previous type systems for ambient calculi, there is a global assignment of types to ambient names.