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.