ABSTRACT
Through the advent of mobile devices and ad hoc communication between these devices, a plethora of issues have been added to the already challenging area of networked distributed computing. The extraordinary dynamism (e.g., node unavailability through mobility) in such settings makes it yet harder to reason about the success of distributed executions. In many cases, nevertheless, one would like to be able to rely on certain actions, or at least have an idea of the state of their completion. In other terms, users and components require guarantees, ideally statically insurable and verifiable, on the interaction (one would want fault tolerance to a certain amount of links, or node failures) in distributed computations, as well as on the data semantics (type safety is desirable for any interaction between two parties) of distributed applications.
