Full development of core modal calculus with motivation and explanatory remarks. Proofs of type preservation, progress, strong normalization, and confluence.
Presents a type theory of mobility and locality based on an S4 modal logic. A simple effect typing system is added to manage store-effects, and mutable references serve as a canonical example of a localized resource. Streamlined presentation of the distributed calculus (compared to the T.R. of '03).
Simpler representation of process ordering and dependencies. Also includes extension with effects (mutable references) showing how the modal type system deals with locality and localized resources. (see revised version published in LOPSTR 2004 proceedings)
Brief presentation of modal calculus with effects and type constructors for concrete datatypes. Marshalling functions are defined, and we consider the existence of marshalling functions for values of various forms of type. Also contains plans and remarks regarding implementation of the operational semantics.