Mobile agent technology supports object migration from one site to another autonomously and proactively, performing its designated location-dependent tasks. Although the concept of proactive mobility has recently been demonstrated in several research prototypes, there is a lack of formal treatment of such mobility from the perspective of a distributed programming language. How to specify, model and reason about travel itineraries of mobile agents is fundamentally important for the development of secure and reliable mobile agent systems.

In this paper, first, we introduce an itinerary language, MAIL, to model the mobile behavior of proactive agents. The language is structured and compositional so that an itinerary can be constructed recursively from primitive itineraries. We then define the operational semantics of the language in terms of a set of inference rules and prove that MAIL is expressive enough for most migration patterns. Finally, we show that MAIL is amenable to formal methods to reason about mobility and verify correctness and safety properties.